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 #
AbsoluteValue.absIsAdmissibleshows the "standard" absolute value on
ℤ, mapping negative
-x, is admissible.
We can partition a finite family into
partition_card ε sets, such that the remainders
in each set are close together.