sumAddHom_apply — Mathlib

English

SumAddHom φ f equals f.sum (x ↦ φ x), i.e., the total image is the sum over all coordinates of φ_i applied to the i-th component.

Русский

SumAddHom φ f равно сумме по всем координатам: сумма φ_i(f_i).

LaTeX

$$$ \\operatorname{sumAddHom} φ f = f.sum \\bigl( x \\mapsto φ x \\bigr). $$$

Lean4

/-- While we didn't need decidable instances to define it, we do to reduce it to a sum -/
theorem sumAddHom_apply [∀ i, AddZeroClass (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [AddCommMonoid γ]
    (φ : ∀ i, β i →+ γ) (f : Π₀ i, β i) : sumAddHom φ f = f.sum fun x => φ x :=
  sumZeroHom_apply _ _

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