Theorems · Theorem · number theory

AbsoluteValue.IsAdmissible.exists_approx

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

Any large enough family of vectors in R^ι 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 98 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

EuclideanDomainFintype