abs_isEuclidean — Mathlib

English

The absolute value on integers is Euclidean.

Русский

Абсолютная величина на целых числах является евклидовой.

LaTeX

$$IsEuclidean(AbsoluteValue.abs : AbsoluteValue Z Z)$$

Lean4

/-- `abs : ℤ → ℤ` is a Euclidean absolute value -/
protected theorem abs_isEuclidean : IsEuclidean (AbsoluteValue.abs : AbsoluteValue ℤ ℤ) :=
  {
    map_lt_map_iff' := fun {x y} =>
      show abs x < abs y ↔ natAbs x < natAbs y by rw [abs_eq_natAbs, abs_eq_natAbs, ofNat_lt] }

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