Commit 2021-09-04 18:18 7729bb6d

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.)