case intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
t : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht : ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
obtain ⟨t, ht⟩ := exists_partition_polynomial_aux n hε hb A
no goals
case intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
t : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht : ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
exact ⟨t, fun i₀ i₁ hi => (ht i₀ i₁).mp hi⟩