feat(algebra): define "Euclidean" absolute values (#8949)
We say an absolute value `abv : absolute_value R S` is Euclidean if agrees with the Euclidean domain structure on `R`, namely `abv x < abv y ↔ euclidean_domain.r x y`.
Examples include `abs : ℤ → ℤ` and `λ (p : polynomial Fq), (q ^ p.degree : ℤ)`, where `Fq` is a finite field with `q` elements. (These two correspond to the number field and function field case respectively, in our proof that the class number of a global field is finite.)
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
