toAdditiveLeft — Mathlib

English

There is an equivalence MonoidHom α (Multiplicative β) ≃ AddMonoidHom (Additive α) β.

Русский

Существует эквивалентность MonoidHom α (Multiplicative β) ≃ AddMonoidHom (Additive α) β.

LaTeX

$$$\text{MonoidHom}(\alpha, \mathrm{Multiplicative}\beta) \simeq \text{AddMonoidHom}(\mathrm{Additive}\alpha, \beta)$$$

Lean4

/-- Reinterpret `α →* Multiplicative β` as `Additive α →+ β`. -/
@[simps!]
def toAdditiveLeft [MulOneClass α] [AddZeroClass β] : (α →* Multiplicative β) ≃ (Additive α →+ β) :=
  AddMonoidHom.toMultiplicativeRight.symm

Похожие утверждения