neg_comp — Mathlib

English

For g1,g2 ∈ M₂ →SL[σ₂₃] M₃ and f ∈ M →SL[σ₁₂] M₂, g1.comp (f1 - f2) = g1.comp f1 - g1.comp f2.

Русский

Для g1,g2 и f1,f2 выполняется g1 ∘ (f1 − f2) = g1 ∘ f1 − g1 ∘ f2.

LaTeX

$$g1.comp (f1 - f2) = g1.comp f1 - g1.comp f2$$

Lean4

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

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