Theorems · Theorem · number theory

AbsoluteValue.exists_partition_int

∀ (n : ℕ) {ε : ℝ},
  0 < ε → ∀ {b : ℤ}, 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.

Defined in

Mathlib.NumberTheory.ClassNumber.AdmissibleAbs

Cited by

0 results in Mathlib

Foundations

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