English
If two AddMonoidHoms f,g from MonoidAlgebra R M to N agree after composing with every singleAddHom m, then f=g.
Русский
Если два AddMonoidHom f,g из MonoidAlgebra R M в N совпадают после композиции с каждым singleAddHom m, то f=g.
LaTeX
$$$\\forall N [AddZeroClass N], \\forall f,g : MonoidAlgebra(R,M) \\to+ N,\\ (\\forall m, f \\circ (singleAddHom m) = g \\circ (singleAddHom m)) \\Rightarrow f = g$$$
Lean4
/-- If two additive homomorphisms from `MonoidAlgebra R M` are equal on each `single r m`,
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)`.
TODO: Rename to `addMonoidHom_ext'`. -/
@[to_additive (attr := ext high) /--
If two additive homomorphisms from `R[M]` are equal on each `single r m`, 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)`.
TODO: Rename to `addMonoidHom_ext'`. -/
]
theorem addHom_ext' {N : Type*} [AddZeroClass N] ⦃f g : MonoidAlgebra R M →+ N⦄
(hfg : ∀ m, f.comp (singleAddHom m) = g.comp (singleAddHom m)) : f = g :=
Finsupp.addHom_ext' hfg
