Admissible absolute value on the integers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file defines an admissible absolute value absolute_value.abs_is_admissible which we use to show the class number of the ring of integers of a number field is finite.

Main results #

absolute_value.abs_is_admissible shows the "standard" absolute value on ℤ, mapping negative x to -x, is admissible.

source

theorem absolute_value.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.

source

noncomputable def absolute_value.abs_is_admissible :

absolute_value.abs.is_admissible

abs : ℤ → ℤ is an admissible absolute value

Equations

absolute_value.abs_is_admissible = {to_is_euclidean := absolute_value.abs_is_admissible._proof_1, card := λ (ε : ℝ), ⌈1 / ε⌉₊, exists_partition' := absolute_value.abs_is_admissible._proof_2}

source

@[protected, instance]

noncomputable def absolute_value.is_admissible.inhabited :

inhabited absolute_value.abs.is_admissible

Equations

absolute_value.is_admissible.inhabited = {default := absolute_value.abs_is_admissible}