Theorems · Theorem · number theory

AbsoluteValue.IsAdmissible.exists_approx_aux

∀ {R : Type u_1} [inst : EuclideanDomain R] {abv : AbsoluteValue R ℤ} (n : ℕ) (h : abv.IsAdmissible) {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (h.card ε ^ n).succ → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε

Any large enough family of vectors in R^n has a pair of elements whose remainders are close together, pointwise.

Defined in

Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue

Cited by

1 results in Mathlib

Foundations

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

Assumes

EuclideanDomain