Euclidean absolute values #

This file defines a predicate AbsoluteValue.IsEuclidean abv stating the absolute value is compatible with the Euclidean domain structure on its domain.

Main definitions #

• AbsoluteValue.IsEuclidean abv is a predicate on absolute values on R mapping to S that preserve the order on R arising from the Euclidean domain structure.
• AbsoluteValue.abs_isEuclidean shows the "standard" absolute value on ℤ, mapping negative x to -x, is euclidean.
structure AbsoluteValue.IsEuclidean {R : Type u_1} {S : Type u_2} [] [] (abv : ) :

An absolute value abv : R → S is Euclidean if it is compatible with the EuclideanDomain structure on R, namely abv is strictly monotone with respect to the well founded relation ≺ on R.

• map_lt_map_iff' : ∀ {x y : R}, abv x < abv y

The requirement of a Euclidean absolute value that abv is monotone with respect to ≺

Instances For
theorem AbsoluteValue.IsEuclidean.map_lt_map_iff' {R : Type u_1} {S : Type u_2} [] [] {abv : } (self : abv.IsEuclidean) {x : R} {y : R} :
abv x < abv y

The requirement of a Euclidean absolute value that abv is monotone with respect to ≺

@[simp]
theorem AbsoluteValue.IsEuclidean.map_lt_map_iff {R : Type u_1} {S : Type u_2} [] [] {abv : } {x : R} {y : R} (h : abv.IsEuclidean) :
abv x < abv y
theorem AbsoluteValue.IsEuclidean.sub_mod_lt {R : Type u_1} {S : Type u_2} [] [] {abv : } (h : abv.IsEuclidean) (a : R) {b : R} (hb : b 0) :
abv (a % b) < abv b
theorem AbsoluteValue.abs_isEuclidean :
AbsoluteValue.abs.IsEuclidean

abs : ℤ → ℤ is a Euclidean absolute value