Theorems · Theorem · number theory

AbsoluteValue.IsAdmissible.exists_partition

∀ {R : Type u_1} [inst : EuclideanDomain R] {abv : AbsoluteValue R ℤ} {ι : Type u_2} [Finite ι] {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : ι → R) (h : abv.IsAdmissible), ∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε

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.

Defined in

Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue

Cited by

1 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

EuclideanDomainFinite