toMultiplicative — Mathlib

English

There is an equivalence AddMonoidHom α β ≃ (Multiplicative α →* Multiplicative β).

Русский

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

LaTeX

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

Lean4

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

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