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} [EuclideanDomain R] [OrderedSemiring S] (abv : AbsoluteValue R S) : Prop

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 ↔ EuclideanDomain.r x y

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

theorem AbsoluteValue.IsEuclidean.map_lt_map_iff' {R : Type u_1} {S : Type u_2} [EuclideanDomain R] [OrderedSemiring S] {abv : AbsoluteValue R S} (self : abv.IsEuclidean) {x : R} {y : R} : abv x < abv y ↔ EuclideanDomain.r x 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} [EuclideanDomain R] [OrderedSemiring S] {abv : AbsoluteValue R S} {x : R} {y : R} (h : abv.IsEuclidean) : abv x < abv y ↔ EuclideanDomain.r x y

theorem AbsoluteValue.IsEuclidean.sub_mod_lt {R : Type u_1} {S : Type u_2} [EuclideanDomain R] [OrderedSemiring S] {abv : AbsoluteValue R S} (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