comp_sub — Mathlib

English

For scalar c in S₃, h ∈ M₂ →SL[σ₂₃] M₃ and f ∈ M →SL[σ₁₂] M₂, (c • h).comp f = c • (h.comp f).

Русский

Для скаляра c ∈ S₃, h и f выполняется (c • h) ∘ f = c • (h ∘ f).

LaTeX

$$ (c • h).comp f = c • h.comp f$$

Lean4

@[simp]
theorem comp_sub [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [IsTopologicalAddGroup M₂] [IsTopologicalAddGroup M₃]
    (g : M₂ →SL[σ₂₃] M₃) (f₁ f₂ : M →SL[σ₁₂] M₂) : g.comp (f₁ - f₂) = g.comp f₁ - g.comp f₂ :=
  by
  ext
  simp

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