Theorems · Theorem · number theory

Polynomial.exists_approx_polynomial

∀ {Fq : Type u_1} [inst : Fintype Fq] [inst_1 : Field Fq] {b : Polynomial Fq},
  b ≠ 0 →
    ∀ {ε : ℝ},
      0 < ε →
        ∀ (A : Fin (Fintype.card Fq ^ ⌈-Real.log ε / Real.log ↑(Fintype.card Fq)⌉₊).succ → Polynomial Fq),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(Polynomial.cardPowDegree (A i₁ % b - A i₀ % b)) < Polynomial.cardPowDegree b • ε

If A is a family of enough low-degree polynomials over a finite field, there is a pair of elements in A (with different indices but not necessarily distinct), such that the difference of their remainders is close together.

Defined in

Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeField