toMultiplicativeRight — Mathlib

English

Extends Additive α →+ β to α →* Multiplicative β via toMul and ofAdd.

Русский

Расширяем Additive α →+ β до α →* Multiplicative β через toMul и ofAdd.

LaTeX

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

Lean4

/-- Reinterpret `Additive α →+ β` as `α →* Multiplicative β`. -/
@[simps]
def toMultiplicativeRight [MulOneClass α] [AddZeroClass β] : (Additive α →+ β) ≃ (α →* Multiplicative β)
    where
  toFun
    f :=
    { toFun := fun a => ofAdd (f (ofMul a))
      map_mul' := f.map_add
      map_one' := f.map_zero }
  invFun
    f :=
    { toFun := fun a => (f a.toMul).toAdd
      map_add' := f.map_mul
      map_zero' := f.map_one }

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