absHom — Mathlib

English

The absolute value extends to a monoid-with-zero hom: toFun = |·|, with map_zero = 0, map_one = 1, and map_mul = (|ab| = |a||b|).

Русский

Модуль распространяется на однородный гомоморфизм: toFun = |·|, map_zero = 0, map_one = 1, и map_mul = (|ab| = |a||b|).

LaTeX

$$absHom : α \to_*₀ α with toFun = |·|, map_zero' = |0| = 0, map_one' = |1| = 1, map_mul' = (|ab| = |a||b|)$$

Lean4

/-- `abs` as a `MonoidWithZeroHom`. -/
def absHom : α →*₀ α where
  toFun := abs
  map_zero' := abs_zero
  map_one' := abs_one
  map_mul' := abs_mul

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