English
If two Additive α →+ β maps have the same multiplicative reinterpretation, then they are equal.
Русский
Если два аддитивных отображения из Additive α в β имеют одинаковое мультипликативное переосмысление, они равны.
LaTeX
$$$\\forall f,g:\\mathrm{Additive}\\alpha \\to_+ \\beta,\n\\; f^{\\mathrm{toMultiplicativeRight}} = g^{\\mathrm{toMultiplicativeRight}} \\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 `α →* Multiplicative β` from equality in `Additive α →+ β`. -/
@[ext]
theorem addMonoidHom_ext [MulOneClass α] [AddZeroClass β] (f g : Additive α →+ β)
(h : f.toMultiplicativeRight = g.toMultiplicativeRight) : f = g :=
AddMonoidHom.toMultiplicativeRight.injective h
