smulRight_eq_comp — Mathlib

English

There is an equality between right smul action and composition with identity on the left.

Русский

Существует равенство между правым действием скаляра и композицией с тождественным отображением слева.

LaTeX

$$$ f.smulRight z = (LinearMap.id.smulRight z).compAlternatingMap f $$$

Lean4

theorem smulRight_eq_comp {R M₁ M₂ ι : Type*} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁]
    [Module R M₂] (f : M₁ [⋀^ι]→ₗ[R] R) (z : M₂) : f.smulRight z = (LinearMap.id.smulRight z).compAlternatingMap f :=
  rfl

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