# mathlib3documentation

algebra.order.euclidean_absolute_value

# Euclidean absolute values #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main definitions #

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

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

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

abs : ℤ → ℤ is a Euclidean absolute value