natAbsHom — Mathlib

English

The natural absolute value map Int.natAbs defines a MonoidWithZeroHom from ℤ to ℕ.

Русский

Функция natAbs задаёт гомоморфизм моноида с нулём из ℤ в ℕ.

LaTeX

$$$\\text{natAbsHom} : \\mathbb{Z} \\to_{0}^{*} \\mathbb{N},\\; \\text{toFun} = |\\cdot|,\\; \\text{map\_mul}' = \\mathrm{natAbs\\_mul},\\; \\text{map\_one}' = \\ \\mathrm{natAbs\\_one},\\; \\text{map\_zero}' = \\ \\mathrm{natAbs\\_zero}$$$

Lean4

/-- `Int.natAbs` as a bundled `MonoidWithZeroHom`. -/
@[simps]
def natAbsHom : ℤ →*₀ ℕ where
  toFun := Int.natAbs
  map_mul' := Int.natAbs_mul
  map_one' := Int.natAbs_one
  map_zero' := Int.natAbs_zero

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