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

• AbsoluteValue.absIsAdmissible shows the "standard" absolute value on ℤ, mapping negative x to -x, is admissible.

theorem AbsoluteValue.exists_partition_int (n : ℕ) {ε : ℝ} (hε : 0 < ε) {b : ℤ} (hb : b ≠ 0) (A : Fin n → ℤ) : ∃ (t : Fin n → Fin ⌈1 / ε⌉₊), ∀ (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.

Equations

• AbsoluteValue.absIsAdmissible = let __src := AbsoluteValue.abs_isEuclidean; { toIsEuclidean := __src, card := fun (ε : ℝ) => ⌈1 / ε⌉₊, exists_partition' := ⋯ }

noncomputable instance AbsoluteValue.instInhabitedIsAdmissibleIntEuclideanDomainAbsToLinearOrderedRingLinearOrderedCommRing : Inhabited (AbsoluteValue.IsAdmissible AbsoluteValue.abs)

Equations

• AbsoluteValue.instInhabitedIsAdmissibleIntEuclideanDomainAbsToLinearOrderedRingLinearOrderedCommRing = { default := AbsoluteValue.absIsAdmissible }