English
If two additive homomorphisms from Finsupp α M to N agree on every singleton a ↦ b, then they are equal overall.
Русский
Если два аддитивных однородных отображения от Finsupp α M в N совпадают на каждом базовом элементе-одиночке a ↦ b, то они совпадают во всей области определения.
LaTeX
$$$\\forall f,g : (\\alpha \\to_0 M) \\to_+ N,\\ (\\forall x,y,\\ f(\\mathrm{single}(x,y)) = g(\\mathrm{single}(x,y))) \\Rightarrow f = g$$$
Lean4
/-- If two additive homomorphisms from `α →₀ M` are equal on each `single a b`,
then they are equal. -/
theorem addHom_ext [AddZeroClass N] ⦃f g : (α →₀ M) →+ N⦄ (H : ∀ x y, f (single x y) = g (single x y)) : f = g :=
by
refine AddMonoidHom.eq_of_eqOn_denseM add_closure_setOf_eq_single ?_
rintro _ ⟨x, y, rfl⟩
apply H
