mathlib

ded0d640 - feat(number_theory): define "admissible" absolute values (#8964)

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. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>