# Documentation

Mathlib.Algebra.Order.EuclideanAbsoluteValue

# 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} [inst : ] [inst : ] (abv : ) :
• The requirement of a Euclidean absolute value that abv is monotone with respect to ≺≺

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

An absolute value abv : R → S→ 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.

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

abs : ℤ → ℤ→ ℤ is a Euclidean absolute value