coe_smul_linearMap — Mathlib

English

There is a natural-number scalar action on LieDerivation R L M making it a SMulBracketCommClass Nat L M, i.e., Nat acts compatibly with the Lie bracket.

Русский

Существует естественное действие натуральных чисел на LieDerivation R L M, приводящее LieDerivation в SMulBracketCommClass Nat L M; т. е. Nat действует согласованно со скобкой Ли.

LaTeX

$$$\text{LieDerivation.SMulBracketCommClass Nat L M}$$$

Lean4

@[simp]
theorem coe_smul_linearMap (r : S) (D : LieDerivation R L M) : ↑(r • D) = r • (D : L →ₗ[R] M) :=
  rfl

Похожие утверждения