English
If two additive homomorphisms f, g from DFinsupp agree on every single i y, then f = g.
Русский
Если два аддитивных гомоморфа f, g сдаются равными на каждом элементе single i y, тогда f = g.
LaTeX
$$$\\forall i,y: f(\\mathrm{single}(i,y)) = g(\\mathrm{single}(i,y)) \\Rightarrow f = g$$$
Lean4
/-- If two additive homomorphisms from `Π₀ i, β i` are equal on each `single a b`, then
they are equal. -/
theorem addHom_ext {γ : Type w} [AddZeroClass γ] ⦃f g : (Π₀ i, β i) →+ γ⦄
(H : ∀ (i : ι) (y : β i), f (single i y) = g (single i y)) : f = g :=
by
refine AddMonoidHom.eq_of_eqOn_denseM add_closure_iUnion_range_single fun f hf => ?_
simp only [Set.mem_iUnion, Set.mem_range] at hf
rcases hf with ⟨x, y, rfl⟩
apply H
