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 #
An absolute value
abv : R → S is Euclidean if it is compatible with the
euclidean_domain structure on
abv is strictly monotone with respect to the well
abs : ℤ → ℤ is a Euclidean absolute value