Theorems · Theorem · number theory

Polynomial.exists_partition_polynomial_aux

∀ {Fq : Type u_1} [inst : Fintype Fq] [inst_1 : Field Fq] (n : ℕ) {ε : ℝ},
  0 < ε →
    ∀ {b : Polynomial Fq},
      b ≠ 0 →
        ∀ (A : Fin n → Polynomial Fq),
          ∃ t,
            ∀ (i₀ i₁ : Fin n),
              t i₀ = t i₁ ↔ ↑(Polynomial.cardPowDegree (A i₁ % b - A i₀ % b)) < Polynomial.cardPowDegree b • ε

A slightly stronger version of exists_partition on which we perform induction on n: for all ε > 0, we can partition the remainders of any family of polynomials A into equivalence classes, where the equivalence(!) relation is "closer than ε".

Defined in

Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeField