English
If two AddMonoidHom from Finsupp α M to N satisfy f.comp (singleAddHom x) = g.comp (singleAddHom x) for all x, then f = g.
Русский
Если два AddMonoidHom из Finsupp α M в N удовлетворяют f ∘ (singleAddHom x) = g ∘ (singleAddHom x) для всех x, то f = g.
LaTeX
$$$\\forall f,g : (\\alpha \\to_0 M) \\to_+ N,\\ (\\forall x, f \\circ (\\mathrm{singleAddHom} x) = g \\circ (\\mathrm{singleAddHom} x)) \\Rightarrow f = g$$$
Lean4
/-- If two additive homomorphisms from `α →₀ M` are equal on each `single a b`,
then they are equal.
We formulate this using equality of `AddMonoidHom`s so that `ext` tactic can apply a type-specific
extensionality lemma after this one. E.g., if the fiber `M` is `ℕ` or `ℤ`, then it suffices to
verify `f (single a 1) = g (single a 1)`. -/
@[ext high]
theorem addHom_ext' [AddZeroClass N] ⦃f g : (α →₀ M) →+ N⦄
(H : ∀ x, f.comp (singleAddHom x) = g.comp (singleAddHom x)) : f = g :=
addHom_ext fun x => DFunLike.congr_fun (H x)
