toMonoidHomEquiv — Mathlib

English

Additive characters A → M are naturally equivalent to monoid homomorphisms from Multiplicative A to M.

Русский

Аддитивные символы A → M естественным образом эквивалентны моноид-гомоморфизмам из Multiplicative A в M.

LaTeX

$$$\mathrm{AddChar}(A,M) \simeq \mathrm{MonoidHom}(\mathrm{Multiplicative} A, M)$$$

Lean4

/-- Additive characters `A → M` are the same thing as monoid homomorphisms from `Multiplicative A`
to `M`. -/
def toMonoidHomEquiv : AddChar A M ≃ (Multiplicative A →* M)
    where
  toFun φ := φ.toMonoidHom
  invFun
    f :=
    { toFun := f.toFun
      map_zero_eq_one' := f.map_one'
      map_add_eq_mul' := f.map_mul' }

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