mathlib3 documentation

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 #

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

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} [euclidean_domain R] [ordered_semiring S] {abv : absolute_value R S} {x y : R} (h : abv.is_euclidean) :
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
@[protected]

abs : ℤ → ℤ is a Euclidean absolute value