abvHom' — Mathlib

English

abv maps R into S as a monoid-with-zero homomorphism; in particular abv(a b) = abv(a) abv(b).

Русский

abv отображает R в S как моноид-гомоморфизм с нулём; в частности abv(a b) = abv(a) abv(b).

LaTeX

$$abv(a b) = abv(a) \cdot abv(b)$$

Lean4

/-- An absolute value as a monoid with zero homomorphism, assuming the target is a semifield. -/
def abvHom' : R →*₀ S where toFun := abv; map_zero' := abv_zero abv; map_one' := abv_one' abv; map_mul' := abv_mul abv

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