Admissible absolute value on the integers #

This file defines an admissible absolute value AbsoluteValue.absIsAdmissible which we use to show the class number of the ring of integers of a number field is finite.

Main results #

theorem AbsoluteValue.exists_partition_int (n : ) {ε : } (hε : 0 < ε) {b : } (hb : b 0) (A : Fin n) :
t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁|A i₁ % b - A i₀ % b| < |b| ε

We can partition a finite family into partition_card ε sets, such that the remainders in each set are close together.

noncomputable def AbsoluteValue.absIsAdmissible :
AbsoluteValue.IsAdmissible AbsoluteValue.abs

abs : ℤ → ℤ is an admissible absolute value.

Instances For