instSMul — Mathlib

English

For any scalar r from S, the underlying function of the scaled derivation r • D is the scalar action of r on the underlying function of D: ↑(r • D) = r • ↑D.

Русский

Для любого скаляра r из S соответствующая функция масштабаемой производной r • D равна действию скаляра r на соответствующую функцию D: ↑(r • D) = r • ↑D.

LaTeX

$$$↑(r \cdot D) = r \cdot ↑D$$$

Lean4

instance instSMul : SMul S (LieDerivation R L M) where
  smul r
    D :=
    { toLinearMap := r • D
      leibniz' := fun a b => by
        simp only [LinearMap.smul_apply, coeFn_coe, apply_lie_eq_sub, smul_sub,
          SMulBracketCommClass.smul_bracket_comm] }

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