English
For any finitely supported family f = (f_i)_i with components f_i ∈ β_i, the value of sumZeroHom φ at f is the finite sum over i of φ_i(f_i).
Русский
Для конечной опоры f = (f_i)_i c компонентами f_i ∈ β_i, значение sumZeroHom φ в f равно конечной сумме по i от φ_i(f_i).
LaTeX
$$$ \\operatorname{sumZeroHom} φ \\, f = \\sum_{i \\in \\operatorname{supp}(f)} φ_i(f_i). $$$
Lean4
/-- While we didn't need decidable instances to define it, we do to reduce it to a sum -/
theorem sumZeroHom_apply [∀ i, AddZeroClass (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [AddCommMonoid γ]
(φ : ∀ i, ZeroHom (β i) γ) (f : Π₀ i, β i) : sumZeroHom φ f = f.sum fun x => φ x :=
by
rcases f with ⟨f, s, hf⟩
change (∑ i ∈ _, _) = ∑ i ∈ _ with _, _
rw [Finset.sum_filter, Finset.sum_congr rfl]
intro i _
dsimp only [coe_mk', Subtype.coe_mk] at *
split_ifs with h
· rfl
· rw [not_not.mp h, map_zero]
