Commit 2021-09-08 06:17 ded0d640

feat(number_theory): define "admissible" absolute values (#8964) We say an absolute value abv : absolute_value R ℤ is admissible if it agrees with the Euclidean domain structure on R (see also is_euclidean in #8949), and large enough sets of elements in R^n contain two elements whose remainders are close together. Examples include abs : ℤ → ℤ and card_pow_degree := λ (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.) Proving these two are indeed admissible involves a lot of pushing values between ℤ and ℝ, but is otherwise not so exciting.