toAddMonoidHom — Mathlib

English

If φ is a MonoidHom from Multiplicative A to M, then the symm maps a to φ(Multiplicative.ofAdd a).

Русский

Если φ — моноид-гомоморфизм от Multiplicative A к M, то симметрично отображение отправляет a в φ(Multiplicative.ofAdd a).

LaTeX

$$toMonoidHomEquiv.symm φ\, a = φ( Multiplicative.ofAdd a )$$

Lean4

/-- Interpret an additive character as a monoid homomorphism. -/
def toAddMonoidHom (φ : AddChar A M) : A →+ Additive M
    where
  toFun := φ.toFun
  map_zero' := φ.map_zero_eq_one'
  map_add' := φ.map_add_eq_mul'

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