sumAddHom_single — Mathlib

English

For AddZeroClass components β_i and γ an additive monoid, sumAddHom φ (single i x) equals φ_i(x).

Русский

Для компонентов β_i и γ, обладающих структурой аддитивной моноида, сумма sumAddHom φ (single i x) равна φ_i(x).

LaTeX

$$$ \\operatorname{sumAddHom} φ (\\mathrm{single } i \\, x) = φ_i(x). $$$

Lean4

@[simp]
theorem sumAddHom_single [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] (φ : ∀ i, β i →+ γ) (i) (x : β i) :
    sumAddHom φ (single i x) = φ i x :=
  sumZeroHom_single _ _ _

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