instDistribMulAction — Mathlib

English

Scalar action on the outer map commutes with composition: (a • g) ∘ f = a • (g ∘ f).

Русский

Действие скаляра на отображение заведомо сохраняет композицию: (a • g) ∘ f = a • (g ∘ f).

LaTeX

$$ (a • g).comp f = a • g.comp f$$

Lean4

instance : DistribMulAction S (M →ₛₗ[σ₁₂] M₂)
    where
  one_smul _ := ext fun _ ↦ one_smul _ _
  mul_smul _ _ _ := ext fun _ ↦ mul_smul _ _ _
  smul_add _ _ _ := ext fun _ ↦ smul_add _ _ _
  smul_zero _ := ext fun _ ↦ smul_zero _

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