English
There is a natural bijection between monoid homomorphisms from the multiplicative form of α to β and additive monoid homomorphisms from α to Additive β, whenever α has an additive structure with zero and β has a multiplicative structure with one.
Русский
Существуют естественная биекция между гомоморфизмами моноидов от мультипликативной структуры α к β и аддитивными гомоморфизмами α → Additive β, при условии, что α имеет аддитивную структуру с нулём, а β — мультипликативную с единицей.
LaTeX
$$$\\mathrm{MonoidHom}(\\mathrm{Multiplicative}\\,\\alpha, \\beta) \\cong (\\alpha \\to_+ \\mathrm{Additive}\\,\\beta)$$$
Lean4
/-- Reinterpret `Multiplicative α →* β` as `α →+ Additive β`. -/
@[simps!]
def toAdditiveRight [AddZeroClass α] [MulOneClass β] : (Multiplicative α →* β) ≃ (α →+ Additive β) :=
AddMonoidHom.toMultiplicativeLeft.symm
