English
The sumZeroHom for Pi.single i φ equals φ composed with the projection to i-th coordinate, i.e., sumZeroHom (Pi.single i φ) = φ ∘ proj_i.
Русский
Сумма sumZeroHom для Pi.single i φ равна φ, композиции с проекцией на i-ю координату, то есть sumZeroHom (Pi.single i φ) = φ ∘ proj_i.
LaTeX
$$$ \\operatorname{sumZeroHom}(\\Pi_{i} \\ φ) = φ \\circ {\\text{proj}_i}. $$$
Lean4
@[simp]
theorem sumAddHom_piSingle [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] (i) (φ : β i →+ γ) :
sumAddHom (Pi.single i φ) = φ.comp (evalAddMonoidHom i) :=
AddMonoidHom.toZeroHom_injective <|
by
convert sumZeroHom_piSingle i φ.toZeroHom using 1
rw [DFinsupp.sumAddHom_toZeroHom]
conv_lhs =>
enter [1, i]
rw [Pi.apply_single (fun i (x : β i →+ γ) => x.toZeroHom) (fun _ => rfl)]
