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.

source

structure absolute_value.is_euclidean {R : Type u_1} {S : Type u_2} [euclidean_domain R] [ordered_semiring S] (abv : absolute_value R S) :

Prop

map_lt_map_iff' : ∀ {x y : R}, ⇑abv x < ⇑abv y ↔ euclidean_domain.r x y

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.

source

@[simp]

theorem absolute_value.is_euclidean.map_lt_map_iff {R : Type u_1} {S : Type u_2} [euclidean_domain R] [ordered_semiring S] {abv : absolute_value R S} {x y : R} (h : abv.is_euclidean) :

⇑abv x < ⇑abv y ↔ euclidean_domain.r x y

source

theorem absolute_value.is_euclidean.sub_mod_lt {R : Type u_1} {S : Type u_2} [euclidean_domain R] [ordered_semiring S] {abv : absolute_value R S} (h : abv.is_euclidean) (a : R) {b : R} (hb : b ≠ 0) :

⇑abv (a % b) < ⇑abv b

source

@[protected]

theorem absolute_value.abs_is_euclidean :

absolute_value.abs.is_euclidean

abs : ℤ → ℤ is a Euclidean absolute value