toMonoidHom — Mathlib

English

An additive character gives a monoid homomorphism from the multiplicative view of A to M.

Русский

Аддитивный характер задаёт моноид-гомоморфизм из мультипликативной структуры A в M.

LaTeX

$$$\mathrm{toMonoidHom}(\varphi): \mathrm{Multiplicative}(A) \to^* M$ defined by $\mathrm{toFun}=\varphi$, $\text{map_zero'}=\varphi(0)=1$, $\text{map_mul'}=\varphi(x+y)$.$$

Lean4

/-- Interpret an additive character as a monoid homomorphism. -/
def toMonoidHom (φ : AddChar A M) : Multiplicative A →* M
    where
  toFun := φ.toFun
  map_one' := φ.map_zero_eq_one'
  map_mul' := φ.map_add_eq_mul'

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