English
If two monoid homomorphisms from Multiplicative α to β have the same additive reinterpretation, then they are equal.
Русский
Если два гомоморфизма моноидов из Multiplicative α в β имеют одинаковое аддитивное переопределение, то они равны.
LaTeX
$$$\\forall f,g:\\mathrm{Multiplicative}\\alpha \\to_* \\beta,\; f^{\\mathrm{toAdditiveRight}} = g^{\\mathrm{toAdditiveRight}} \\Rightarrow f = g$$$
Lean4
/-- This ext lemma moves the type tag to the codomain, since most ext lemmas act on the domain.
WARNING: This has the potential to send `ext` into a loop if someone locally adds the inverse ext
lemma proving equality in `α →+ Additive β` from equality in `Multiplicative α →* β`. -/
@[ext]
theorem monoidHom_ext [AddZeroClass α] [MulOneClass β] (f g : Multiplicative α →* β)
(h : f.toAdditiveRight = g.toAdditiveRight) : f = g :=
MonoidHom.toAdditiveRight.injective h
