comp_neg — Mathlib

English

For suitable rings and spaces, g.comp(-f) = -(g.comp f).

Русский

При подходящих кольцах и пространствах выполняется g ∘ (−f) = −(g ∘ f).

LaTeX

$$g.comp(-f) = -g.comp f$$

Lean4

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

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