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 #

structure AbsoluteValue.IsEuclidean {R : Type u_1} {S : Type u_2} [EuclideanDomain R] [OrderedSemiring S] (abv : AbsoluteValue R S) :

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

Instances For
    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