English
If for all x the equality f.comp (AddMonoidHom.toMultiplicative (singleAddHom x)) = g.comp (AddMonoidHom.toMultiplicative (singleAddHom x)) holds, then f = g.
Русский
Если для каждого x выполняется f ∘ (AddMonoidHom.toMultiplicative (singleAddHom x)) = g ∘ (AddMonoidHom.toMultiplicative (singleAddHom x)), тогда f = g.
LaTeX
$$$\\forall {f g : MonoidHom (Multiplicative (\\alpha \\to_0 M)) N},\\ (\\forall x,\\ f.comp (AddMonoidHom.toMultiplicative (\\mathrm{singleAddHom} x)) = g.comp (AddMonoidHom.toMultiplicative (\\mathrm{singleAddHom} x))) \\Rightarrow f = g$$$
Lean4
@[ext]
theorem mulHom_ext' [MulOneClass N] {f g : Multiplicative (α →₀ M) →* N}
(H :
∀ x,
f.comp (AddMonoidHom.toMultiplicative (singleAddHom x)) =
g.comp (AddMonoidHom.toMultiplicative (singleAddHom x))) :
f = g :=
mulHom_ext fun x => DFunLike.congr_fun (H x)
