Admissible absolute value on the integers #
This file defines an admissible absolute value
which we use to show the class number of the ring of integers of a number field
Main results #
We can partition a finite family into
partition_card ε sets, such that the remainders
in each set are close together.
abs : ℤ → ℤ is an admissible absolute value