Admissible absolute values #
This file defines a structure AbsoluteValue.IsAdmissible
which we use to show the class number
of the ring of integers of a global field is finite.
Main definitions #
AbsoluteValue.IsAdmissible abv
states the absolute valueabv : R → ℤ→ ℤ
respects the Euclidean domain structure onR
, and that a large enough set of elements ofR^n
contains a pair of elements whose remainders are pointwise close together.
Main results #
AbsoluteValue.absIsAdmissible
shows the "standard" absolute value onℤ
, mapping negativex
to-x
, is admissible.Polynomial.cardPowDegreeIsAdmissible
showscardPowDegree
, mappingp : Polynomial 𝔽_q
toq ^ degree p
, is admissible
For all
ε > 0
and finite familiesA
, we can partition the remainders ofA
modb
intoabv.card ε
sets, such that all elements in each part of remainders are close together.
An absolute value R → ℤ→ ℤ
is admissible if it respects the Euclidean domain
structure and a large enough set of elements in R^n
will contain a pair of
elements whose remainders are pointwise close together.
Instances For
For all ε > 0
and finite families A
, we can partition the remainders of A
mod b
into abv.card ε
sets, such that all elements in each part of remainders are close together.
Any large enough family of vectors in R^n
has a pair of elements
whose remainders are close together, pointwise.
Any large enough family of vectors in R^ι
has a pair of elements
whose remainders are close together, pointwise.