Lean4
/-- When summing over an `AddMonoidHom`, the decidability assumption is not needed, and the result is
also an `AddMonoidHom`.
-/
@[simps toZeroHom]
def sumAddHom [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] (φ : ∀ i, β i →+ γ) : (Π₀ i, β i) →+ γ
where
__ := sumZeroHom fun i => φ i |>.toZeroHom
map_add' := by
rintro ⟨f, sf, hf⟩ ⟨g, sg, hg⟩
change (∑ i ∈ _, _) = (∑ i ∈ _, _) + ∑ i ∈ _, _
simp only [AddMonoidHom.toZeroHom_coe, coe_add, coe_mk', Pi.add_apply, map_add, Finset.sum_add_distrib]
congr 1
· refine (Finset.sum_subset ?_ ?_).symm
· intro i
simp only [Multiset.mem_toFinset, Multiset.mem_add]
exact Or.inl
· intro i _ H2
simp only [Multiset.mem_toFinset] at H2
rw [(hf i).resolve_left H2, AddMonoidHom.map_zero]
· refine (Finset.sum_subset ?_ ?_).symm
· intro i
simp only [Multiset.mem_toFinset, Multiset.mem_add]
exact Or.inr
· intro i _ H2
simp only [Multiset.mem_toFinset] at H2
rw [(hg i).resolve_left H2, AddMonoidHom.map_zero]
