AbsoluteValue.IsEuclidean.map_lt_map_iff'
theorem AbsoluteValue.IsEuclidean.map_lt_map_iff' :
∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : OrderedSemiring S] {abv : AbsoluteValue R S},
abv.IsEuclidean → ∀ {x y : R}, abv x < abv y ↔ EuclideanDomain.r x y
This theorem states that for any Euclidean domain `R` and any ordered semiring `S`, and given an absolute value `abv` from `R` to `S`, if `abv` is a Euclidean absolute value, then for any two elements `x` and `y` of `R`, `abv x` is less than `abv y` if and only if `x` is related to `y` by the well-founded relation on `R` defined in the context of Euclidean domain (which ensures the termination of the GCD algorithm). This relation is often denoted `≺` and is defined such that `r (a % b) b` for any `a, b` in `R`. This theorem essentially asserts the monotonicity of the Euclidean absolute value with respect to the `≺` relation.
More concisely: For any Euclidean domain `R` and ordered semiring `S` with Euclidean absolute value `abv` from `R` to `S`, `abv(x) < abv(y)` if and only if `x ≺ y` for all `x, y` in `R`.
|
AbsoluteValue.abs_isEuclidean
theorem AbsoluteValue.abs_isEuclidean : AbsoluteValue.abs.IsEuclidean
The theorem `AbsoluteValue.abs_isEuclidean` states that the absolute value function `abs`, which maps an integer to another integer, behaves as a Euclidean absolute value. In other words, this function upholds the properties that define a Euclidean absolute value in the context of a mathematical structure known as a LinearOrderedRing.
More concisely: The absolute value function on integers is a Euclidean absolute value in the context of a LinearOrderedRing.
|