English
If two multiplicative homomorphisms from Multiplicative (α →₀ M) to N agree on all single x y, then they are equal.
Русский
Если два мультипликативных гомоморфизма из Multiplicative (α →₀ M) в N совпадают на всех элементов вида single x y, то они равны.
LaTeX
$$$\\forall {f g :\\ Multiplicative (\\alpha \\to_0 M) \\to* N},\\ (\\forall x y,\\ f(\\mathrm{single}(x,y)) = g(\\mathrm{single}(x,y))) \\Rightarrow f = g$$$
Lean4
theorem mulHom_ext [MulOneClass N] ⦃f g : Multiplicative (α →₀ M) →* N⦄
(H : ∀ x y, f (Multiplicative.ofAdd <| single x y) = g (Multiplicative.ofAdd <| single x y)) : f = g :=
MonoidHom.ext <|
DFunLike.congr_fun <| by
have := addHom_ext (f := f.toAdditiveRight) (g := g.toAdditiveRight) H
ext
rw [DFunLike.ext_iff] at this
apply this
