Theorems · Inductive type · order theory

AbsoluteValue.IsEuclidean

{R : Type u_1} →
  {S : Type u_2} →
    [inst : EuclideanDomain R] → [inst_1 : Semiring S] → [inst_2 : PartialOrder S] → AbsoluteValue R S → Prop

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.

Defined in

Mathlib.Algebra.Order.AbsoluteValue.Euclidean

Cited by

9 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

EuclideanDomainSemiringPartialOrder