Definition
For any prime number $p$ and natural number $n$, we can define a polynomial
\[f_{p,n}:=X^{p-1}(X-1)^p\cdots(X-n)^p\]
def f_p (p : ℕ) (hp : nat.prime p) (n : ℕ): ℤ[X] := polynomial.X ^ (p - 1) * (∏ i in finset.range n, (polynomial.X - (polynomial.C (i+1:ℤ)))^p)
Theorem
The degree of $f_{p,n}$ is $(n+1)p-1$
-
polynomial.nat_degree_mul_eqasserts that the degree of $pq$ is degree of $p$ plus degree of $q$ provided $p$ and $q$ are nonzero -
prod_degasserts that degree of $\prod_{i} p_i$ equals $\sum_i,\mathrm {degree of } p_i$ provided that for all $i,p_i\ne 0$.
lemma deg_f_p (p : ℕ) (hp : nat.prime p) (n : ℕ) : (f_p p hp n).nat_degree = (n+1)*p - 1 :=
Proof
QED.
So we have degree of
f_p is degree of $X^{p-1}$ plus degree of $(X-1)^p\cdots(X-n)^p$
have eq1 := @polynomial.nat_degree_mul ℤ _ (polynomial.X ^ (p - 1)) (∏ i in finset.range n, (polynomial.X - (polynomial.C (i+1:ℤ)))^p) _ _,
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ (polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(n + 1) * p - 1
3 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree
⊢ (polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(n + 1) * p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
rw eq1,
3 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree
⊢ (polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(n + 1) * p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
3 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree
⊢ (polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(n + 1) * p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
simp only [int.cast_coe_nat, mul_one, polynomial.nat_degree_X, int.cast_add, ring_hom.eq_int_cast, int.cast_one, polynomial.nat_degree_pow],
3 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree
⊢ (polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(n + 1) * p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
3 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree
⊢ p - 1 + (∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree = (n + 1) * p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
degree of $(X-1)^p\cdots(X-n)^p$ is $p\times$(degree of $(X-1)$+degree of $(X-2)$+...+ degree of $(X-n)$)
have triv' : (∏ (i : ℕ) in finset.range n, (polynomial.X - polynomial.C (i+1:ℤ)) ^ p).nat_degree
3 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree
⊢ p - 1 + (∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree = (n + 1) * p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
3 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree
⊢ p - 1 + (∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree = (n + 1) * p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
= ∑ i in finset.range n, ((polynomial.X - polynomial.C (i+1:ℤ)) ^ p).nat_degree,
3 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree
⊢ p - 1 + (∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree = (n + 1) * p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
4 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree
⊢ (∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, ((polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, ((polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree
⊢ p - 1 + (∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree = (n + 1) * p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
{
4 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree
⊢ (∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, ((polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, ((polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree
⊢ p - 1 + (∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree = (n + 1) * p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree
⊢ (∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, ((polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree
apply prod_deg,
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree
⊢ (∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, ((polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree
⊢ ∀ (i : ℕ), i ∈ finset.range n → (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
intros i hi, intro rid,
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree
⊢ ∀ (i : ℕ), i ∈ finset.range n → (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
i : ℕ,
hi : i ∈ finset.range n,
rid : (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p = 0
⊢ false
replace rid := @pow_eq_zero (ℤ[X]) _ _ (polynomial.X - polynomial.C (i+1:ℤ)) p rid,
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
i : ℕ,
hi : i ∈ finset.range n,
rid : (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p = 0
⊢ false
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
i : ℕ,
hi : i ∈ finset.range n,
rid : polynomial.X - ⇑polynomial.C (↑i + 1) = 0
⊢ false
rw sub_eq_zero_iff_eq at rid,
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
i : ℕ,
hi : i ∈ finset.range n,
rid : polynomial.X - ⇑polynomial.C (↑i + 1) = 0
⊢ false
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
i : ℕ,
hi : i ∈ finset.range n,
rid : polynomial.X = ⇑polynomial.C (↑i + 1)
⊢ false
have rid' : (polynomial.C (i+1:ℤ)).nat_degree = 1,
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
i : ℕ,
hi : i ∈ finset.range n,
rid : polynomial.X = ⇑polynomial.C (↑i + 1)
⊢ false
2 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
i : ℕ,
hi : i ∈ finset.range n,
rid : polynomial.X = ⇑polynomial.C (↑i + 1)
⊢ (⇑polynomial.C (↑i + 1)).nat_degree = 1
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
i : ℕ,
hi : i ∈ finset.range n,
rid : polynomial.X = ⇑polynomial.C (↑i + 1),
rid' : (⇑polynomial.C (↑i + 1)).nat_degree = 1
⊢ false
rw <-rid, exact polynomial.nat_degree_X, have rid'' := polynomial.nat_degree_C (i+1:ℤ), linarith,
2 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
i : ℕ,
hi : i ∈ finset.range n,
rid : polynomial.X = ⇑polynomial.C (↑i + 1)
⊢ (⇑polynomial.C (↑i + 1)).nat_degree = 1
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
i : ℕ,
hi : i ∈ finset.range n,
rid : polynomial.X = ⇑polynomial.C (↑i + 1),
rid' : (⇑polynomial.C (↑i + 1)).nat_degree = 1
⊢ false
no goals
},
no goals
3 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, ((polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree
⊢ p - 1 + (∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree = (n + 1) * p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
simp only [int.cast_coe_nat, int.cast_add, ring_hom.eq_int_cast, int.cast_one, polynomial.nat_degree_pow] at triv',
3 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, ((polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree
⊢ p - 1 + (∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree = (n + 1) * p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
3 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree
⊢ p - 1 + (∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree = (n + 1) * p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
rw triv',
3 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree
⊢ p - 1 + (∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree = (n + 1) * p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
3 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree
⊢ p - 1 + ∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree = (n + 1) * p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
each of $(X-i)^p$ has degree p. So The sum of degree is n*p.
have triv'' : (∑ (i : ℕ) in finset.range n, p * (polynomial.X - (polynomial.C (i + 1:ℤ))).nat_degree) = ∑ x in finset.range n, p,
3 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree
⊢ p - 1 + ∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree = (n + 1) * p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
4 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree
⊢ ∑ (i : ℕ) in finset.range n, p * (polynomial.X - ⇑polynomial.C (↑i + 1)).nat_degree =
∑ (x : ℕ) in finset.range n, p
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree,
triv'' :
∑ (i : ℕ) in finset.range n, p * (polynomial.X - ⇑polynomial.C (↑i + 1)).nat_degree =
∑ (x : ℕ) in finset.range n, p
⊢ p - 1 + ∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree = (n + 1) * p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
{
4 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree
⊢ ∑ (i : ℕ) in finset.range n, p * (polynomial.X - ⇑polynomial.C (↑i + 1)).nat_degree =
∑ (x : ℕ) in finset.range n, p
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree,
triv'' :
∑ (i : ℕ) in finset.range n, p * (polynomial.X - ⇑polynomial.C (↑i + 1)).nat_degree =
∑ (x : ℕ) in finset.range n, p
⊢ p - 1 + ∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree = (n + 1) * p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree
⊢ ∑ (i : ℕ) in finset.range n, p * (polynomial.X - ⇑polynomial.C (↑i + 1)).nat_degree =
∑ (x : ℕ) in finset.range n, p
apply congr_arg, ext i,
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree
⊢ ∑ (i : ℕ) in finset.range n, p * (polynomial.X - ⇑polynomial.C (↑i + 1)).nat_degree =
∑ (x : ℕ) in finset.range n, p
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree,
i : ℕ
⊢ p * (polynomial.X - ⇑polynomial.C (↑i + 1)).nat_degree = p
rw polynomial.nat_degree_X_sub_C, rw mul_one,
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree,
i : ℕ
⊢ p * (polynomial.X - ⇑polynomial.C (↑i + 1)).nat_degree = p
no goals
},
no goals
3 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree,
triv'' :
∑ (i : ℕ) in finset.range n, p * (polynomial.X - ⇑polynomial.C (↑i + 1)).nat_degree =
∑ (x : ℕ) in finset.range n, p
⊢ p - 1 + ∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree = (n + 1) * p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
simp only [int.cast_coe_nat, int.cast_add, ring_hom.eq_int_cast, nat.cast_id, finset.sum_const, nsmul_eq_mul, int.cast_one, finset.card_range] at triv'' ⊢,
3 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree,
triv'' :
∑ (i : ℕ) in finset.range n, p * (polynomial.X - ⇑polynomial.C (↑i + 1)).nat_degree =
∑ (x : ℕ) in finset.range n, p
⊢ p - 1 + ∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree = (n + 1) * p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
3 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree,
triv'' : ∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree = n * p
⊢ p - 1 + ∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree = (n + 1) * p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
rw triv'', ring,
3 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree,
triv'' : ∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree = n * p
⊢ p - 1 + ∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree = (n + 1) * p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
3 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree,
triv'' : ∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree = n * p
⊢ p - 1 + p * n = p * n + p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
have eq2 := (@nat.add_sub_assoc p 1 _ (p*n)),
3 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree,
triv'' : ∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree = n * p
⊢ p - 1 + p * n = p * n + p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
4 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree,
triv'' : ∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree = n * p,
eq2 : p * n + p - 1 = p * n + (p - 1)
⊢ p - 1 + p * n = p * n + p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree,
triv'' : ∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree = n * p
⊢ 1 ≤ p
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
rw eq2, rw add_comm, exact nat.succ_le_iff.mpr (nat.prime.pos hp),
4 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree,
triv'' : ∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree = n * p,
eq2 : p * n + p - 1 = p * n + (p - 1)
⊢ p - 1 + p * n = p * n + p - 1
p : ℕ,
hp : nat.prime p,
n : ℕ,
eq1 :
(polynomial.X ^ (p - 1) *
∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree =
(polynomial.X ^ (p - 1)).nat_degree +
(∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p).nat_degree,
triv' :
(∏ (i : ℕ) in finset.range n, (polynomial.X - (↑i + 1)) ^ p).nat_degree =
∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree,
triv'' : ∑ (i : ℕ) in finset.range n, p * (polynomial.X - (↑i + 1)).nat_degree = n * p
⊢ 1 ≤ p
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
2 goals
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
intro rid, replace rid := pow_eq_zero rid, exact polynomial.X_ne_zero rid,
2 goals
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ polynomial.X ^ (p - 1) ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
intro rid, rw finset.prod_eq_zero_iff at rid,
p : ℕ,
hp : nat.prime p,
n : ℕ
⊢ ∏ (i : ℕ) in finset.range n, (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p ≠ 0
p : ℕ,
hp : nat.prime p,
n : ℕ,
rid : ∃ (a : ℕ) (H : a ∈ finset.range n), (polynomial.X - ⇑polynomial.C (↑a + 1)) ^ p = 0
⊢ false
choose i hi using rid, have hi2 := hi.2, replace hi2 := pow_eq_zero hi2,
p : ℕ,
hp : nat.prime p,
n : ℕ,
rid : ∃ (a : ℕ) (H : a ∈ finset.range n), (polynomial.X - ⇑polynomial.C (↑a + 1)) ^ p = 0
⊢ false
p : ℕ,
hp : nat.prime p,
n i : ℕ,
hi : i ∈ finset.range n ∧ (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p = 0,
hi2 : polynomial.X - ⇑polynomial.C (↑i + 1) = 0
⊢ false
exact not_not.mpr hi2 (polynomial.X_sub_C_ne_zero (↑i + 1)),
p : ℕ,
hp : nat.prime p,
n i : ℕ,
hi : i ∈ finset.range n ∧ (polynomial.X - ⇑polynomial.C (↑i + 1)) ^ p = 0,
hi2 : polynomial.X - ⇑polynomial.C (↑i + 1) = 0
⊢ false
no goals
Definition
For a prime number $p$ and a polynomial $g$
$$J_p(g):= \sum_{i=0}^d g_i I(f_{p,d},i)$$ where $d$ is the degree of $g$.
def J (g : ℤ[X]) (p : ℕ) (hp : nat.prime p) : ℝ :=
∑ i in finset.range g.nat_degree.succ, (g.coeff i : ℝ) * (II (f_p p hp g.nat_degree) i (nonneg_nat i))
Theorem
$$J_{p}(g) = \sum_{i=0}^d g_i\left(e^i\sum_{j=0}^{(n+1)p-1} f_{p,d}^{(j)}(0)-\sum_{j=0}^{(n+1)p-1}f_{p,d}^{(j)}(i)\right)$
private lemma J_eq1 (g : ℤ[X]) (p : ℕ) (hp : nat.prime p) :
(J g p hp) = ∑ i in finset.range g.nat_degree.succ, (g.coeff i:ℝ) * (I (f_p p hp g.nat_degree) i (nonneg_nat i)) :=
Proof
QED.
x = n.succ
rw mul_eq_zero, right, rw [hx2, deriv_X_sub_pow, polynomial.eval_mul, polynomial.eval_pow],
case or.inr
p : ℕ,
hp : nat.prime p,
n : ℕ,
IH : ∀ (x j : ℕ), j < p → x > 0 → x < n.succ → polynomial.eval ↑x (deriv_n (f_p p hp n) j) = 0,
x j : ℕ,
hj : j < p,
hx1 : x > 0,
y : ℕ,
hy : y < j.succ,
hx2 : x = n.succ
⊢ ↑(j.choose y) * polynomial.eval ↑x (deriv_n (f_p p hp n) (j - y)) *
polynomial.eval ↑x (deriv_n ((polynomial.X - ⇑polynomial.C (↑n + 1)) ^ p) y) =
0
2 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
IH : ∀ (x j : ℕ), j < p → x > 0 → x < n.succ → polynomial.eval ↑x (deriv_n (f_p p hp n) j) = 0,
x j : ℕ,
hj : j < p,
hx1 : x > 0,
y : ℕ,
hy : y < j.succ,
hx2 : x = n.succ
⊢ polynomial.eval ↑(n.succ) (⇑polynomial.C (∏ (i : ℕ) in finset.range y, (↑p - ↑i))) *
polynomial.eval ↑(n.succ) (polynomial.X - ⇑polynomial.C (↑n + 1)) ^ (p - y) =
0
p : ℕ,
hp : nat.prime p,
n : ℕ,
IH : ∀ (x j : ℕ), j < p → x > 0 → x < n.succ → polynomial.eval ↑x (deriv_n (f_p p hp n) j) = 0,
x j : ℕ,
hj : j < p,
hx1 : x > 0,
y : ℕ,
hy : y < j.succ,
hx2 : x = n.succ
⊢ y ≤ p
simp only [polynomial.eval_X, polynomial.eval_C, int.coe_nat_succ, polynomial.eval_sub, sub_self, mul_eq_zero],
2 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
IH : ∀ (x j : ℕ), j < p → x > 0 → x < n.succ → polynomial.eval ↑x (deriv_n (f_p p hp n) j) = 0,
x j : ℕ,
hj : j < p,
hx1 : x > 0,
y : ℕ,
hy : y < j.succ,
hx2 : x = n.succ
⊢ polynomial.eval ↑(n.succ) (⇑polynomial.C (∏ (i : ℕ) in finset.range y, (↑p - ↑i))) *
polynomial.eval ↑(n.succ) (polynomial.X - ⇑polynomial.C (↑n + 1)) ^ (p - y) =
0
p : ℕ,
hp : nat.prime p,
n : ℕ,
IH : ∀ (x j : ℕ), j < p → x > 0 → x < n.succ → polynomial.eval ↑x (deriv_n (f_p p hp n) j) = 0,
x j : ℕ,
hj : j < p,
hx1 : x > 0,
y : ℕ,
hy : y < j.succ,
hx2 : x = n.succ
⊢ y ≤ p
2 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
IH : ∀ (x j : ℕ), j < p → x > 0 → x < n.succ → polynomial.eval ↑x (deriv_n (f_p p hp n) j) = 0,
x j : ℕ,
hj : j < p,
hx1 : x > 0,
y : ℕ,
hy : y < j.succ,
hx2 : x = n.succ
⊢ ∏ (i : ℕ) in finset.range y, (↑p - ↑i) = 0 ∨ 0 ^ (p - y) = 0
p : ℕ,
hp : nat.prime p,
n : ℕ,
IH : ∀ (x j : ℕ), j < p → x > 0 → x < n.succ → polynomial.eval ↑x (deriv_n (f_p p hp n) j) = 0,
x j : ℕ,
hj : j < p,
hx1 : x > 0,
y : ℕ,
hy : y < j.succ,
hx2 : x = n.succ
⊢ y ≤ p
right, apply zero_pow (nat.sub_pos_of_lt (gt_of_ge_of_gt hj hy)),
2 goals
p : ℕ,
hp : nat.prime p,
n : ℕ,
IH : ∀ (x j : ℕ), j < p → x > 0 → x < n.succ → polynomial.eval ↑x (deriv_n (f_p p hp n) j) = 0,
x j : ℕ,
hj : j < p,
hx1 : x > 0,
y : ℕ,
hy : y < j.succ,
hx2 : x = n.succ
⊢ ∏ (i : ℕ) in finset.range y, (↑p - ↑i) = 0 ∨ 0 ^ (p - y) = 0
p : ℕ,
hp : nat.prime p,
n : ℕ,
IH : ∀ (x j : ℕ), j < p → x > 0 → x < n.succ → polynomial.eval ↑x (deriv_n (f_p p hp n) j) = 0,
x j : ℕ,
hj : j < p,
hx1 : x > 0,
y : ℕ,
hy : y < j.succ,
hx2 : x = n.succ
⊢ y ≤ p
p : ℕ,
hp : nat.prime p,
n : ℕ,
IH : ∀ (x j : ℕ), j < p → x > 0 → x < n.succ → polynomial.eval ↑x (deriv_n (f_p p hp n) j) = 0,
x j : ℕ,
hj : j < p,
hx1 : x > 0,
y : ℕ,
hy : y < j.succ,
hx2 : x = n.succ
⊢ y ≤ p
exact le_of_lt (gt_of_ge_of_gt hj hy),
p : ℕ,
hp : nat.prime p,
n : ℕ,
IH : ∀ (x j : ℕ), j < p → x > 0 → x < n.succ → polynomial.eval ↑x (deriv_n (f_p p hp n) j) = 0,
x j : ℕ,
hj : j < p,
hx1 : x > 0,
y : ℕ,
hy : y < j.succ,
hx2 : x = n.succ
⊢ y ≤ p
no goals
},
no goals
no goals
}
no goals
no goals
main part
intro e_algebraic,
⊢ transcendental e
e_algebraic : is_algebraic ℤ e
⊢ false
rw is_algebraic at e_algebraic,
e_algebraic : is_algebraic ℤ e
⊢ false
e_algebraic : ∃ (p : ℤ[X]), p ≠ 0 ∧ ⇑(polynomial.aeval e) p = 0
⊢ false
choose g' g'_def using e_algebraic,
e_algebraic : ∃ (p : ℤ[X]), p ≠ 0 ∧ ⇑(polynomial.aeval e) p = 0
⊢ false
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0
⊢ false
have g'_nonzero := g'_def.1,
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0
⊢ false
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0
⊢ false
have e_root_g' := g'_def.2,
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0
⊢ false
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0
⊢ false
generalize g_def : make_const_term_nonzero g' g'_nonzero = g,
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0
⊢ false
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g
⊢ false
have coeff_zero_nonzero : (g.coeff 0) ≠ 0,
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g
⊢ false
2 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g
⊢ g.coeff 0 ≠ 0
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0
⊢ false
rw <-g_def, apply coeff_zero_after_change,
2 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g
⊢ g.coeff 0 ≠ 0
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0
⊢ false
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0
⊢ false
have e_root_g : (@polynomial.aeval ℤ ℝ _ _ _ e) g = 0,
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0
⊢ false
2 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0
⊢ ⇑(polynomial.aeval e) g = 0
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ false
rw <-g_def,
2 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0
⊢ ⇑(polynomial.aeval e) g = 0
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ false
2 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0
⊢ ⇑(polynomial.aeval e) (make_const_term_nonzero g' g'_nonzero) = 0
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ false
apply non_zero_root_same, rw e, exact (1:ℝ).exp_ne_zero, exact e_root_g',
2 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0
⊢ ⇑(polynomial.aeval e) (make_const_term_nonzero g' g'_nonzero) = 0
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ false
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ false
have coup_de_grace := coup_de_grace (M g) _ (max g.nat_degree (abs (g.coeff 0))),
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ false
2 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
coup_de_grace :
∃ (p : nat.primes), ↑(p.val) > max ↑(g.nat_degree) (abs (g.coeff 0)) ∧ ↑((p.val - 1).fact) > M g ^ p.val
⊢ false
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ M g ≥ 0
choose p Hp using coup_de_grace,
2 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
coup_de_grace :
∃ (p : nat.primes), ↑(p.val) > max ↑(g.nat_degree) (abs (g.coeff 0)) ∧ ↑((p.val - 1).fact) > M g ^ p.val
⊢ false
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ M g ≥ 0
2 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
Hp : ↑(p.val) > max ↑(g.nat_degree) (abs (g.coeff 0)) ∧ ↑((p.val - 1).fact) > M g ^ p.val
⊢ false
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ M g ≥ 0
have abs_J_upper_bound := abs_J_upper_bound g p.val p.property,
2 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
Hp : ↑(p.val) > max ↑(g.nat_degree) (abs (g.coeff 0)) ∧ ↑((p.val - 1).fact) > M g ^ p.val
⊢ false
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ M g ≥ 0
2 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
Hp : ↑(p.val) > max ↑(g.nat_degree) (abs (g.coeff 0)) ∧ ↑((p.val - 1).fact) > M g ^ p.val,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val
⊢ false
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ M g ≥ 0
simp only [gt_iff_lt, max_lt_iff, int.coe_nat_lt] at Hp,
2 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
Hp : ↑(p.val) > max ↑(g.nat_degree) (abs (g.coeff 0)) ∧ ↑((p.val - 1).fact) > M g ^ p.val,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val
⊢ false
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ M g ≥ 0
2 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val,
Hp : (g.nat_degree < p.val ∧ abs (g.coeff 0) < ↑(p.val)) ∧ M g ^ p.val < ↑((p.val - 1).fact)
⊢ false
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ M g ≥ 0
have abs_J_lower_bound := abs_J_lower_bound g e_root_g coeff_zero_nonzero p.val p.property _,
2 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val,
Hp : (g.nat_degree < p.val ∧ abs (g.coeff 0) < ↑(p.val)) ∧ M g ^ p.val < ↑((p.val - 1).fact)
⊢ false
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ M g ≥ 0
3 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val,
Hp : (g.nat_degree < p.val ∧ abs (g.coeff 0) < ↑(p.val)) ∧ M g ^ p.val < ↑((p.val - 1).fact),
abs_J_lower_bound : ↑((p.val - 1).fact) ≤ abs (J g p.val _)
⊢ false
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val,
Hp : (g.nat_degree < p.val ∧ abs (g.coeff 0) < ↑(p.val)) ∧ M g ^ p.val < ↑((p.val - 1).fact)
⊢ p.val > g.nat_degree ∧ p.val > (g.coeff 0).nat_abs
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ M g ≥ 0
have rid := le_trans abs_J_lower_bound abs_J_upper_bound,
3 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val,
Hp : (g.nat_degree < p.val ∧ abs (g.coeff 0) < ↑(p.val)) ∧ M g ^ p.val < ↑((p.val - 1).fact),
abs_J_lower_bound : ↑((p.val - 1).fact) ≤ abs (J g p.val _)
⊢ false
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val,
Hp : (g.nat_degree < p.val ∧ abs (g.coeff 0) < ↑(p.val)) ∧ M g ^ p.val < ↑((p.val - 1).fact)
⊢ p.val > g.nat_degree ∧ p.val > (g.coeff 0).nat_abs
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ M g ≥ 0
3 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val,
Hp : (g.nat_degree < p.val ∧ abs (g.coeff 0) < ↑(p.val)) ∧ M g ^ p.val < ↑((p.val - 1).fact),
abs_J_lower_bound : ↑((p.val - 1).fact) ≤ abs (J g p.val _),
rid : ↑((p.val - 1).fact) ≤ M g ^ p.val
⊢ false
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val,
Hp : (g.nat_degree < p.val ∧ abs (g.coeff 0) < ↑(p.val)) ∧ M g ^ p.val < ↑((p.val - 1).fact)
⊢ p.val > g.nat_degree ∧ p.val > (g.coeff 0).nat_abs
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ M g ≥ 0
have rid2 := Hp.right, replace rid2 : ¬ ((M g ^ p) ≥ ((p.val - 1).fact:ℝ)) := not_le.mpr rid2,
3 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val,
Hp : (g.nat_degree < p.val ∧ abs (g.coeff 0) < ↑(p.val)) ∧ M g ^ p.val < ↑((p.val - 1).fact),
abs_J_lower_bound : ↑((p.val - 1).fact) ≤ abs (J g p.val _),
rid : ↑((p.val - 1).fact) ≤ M g ^ p.val
⊢ false
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val,
Hp : (g.nat_degree < p.val ∧ abs (g.coeff 0) < ↑(p.val)) ∧ M g ^ p.val < ↑((p.val - 1).fact)
⊢ p.val > g.nat_degree ∧ p.val > (g.coeff 0).nat_abs
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ M g ≥ 0
3 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val,
Hp : (g.nat_degree < p.val ∧ abs (g.coeff 0) < ↑(p.val)) ∧ M g ^ p.val < ↑((p.val - 1).fact),
abs_J_lower_bound : ↑((p.val - 1).fact) ≤ abs (J g p.val _),
rid : ↑((p.val - 1).fact) ≤ M g ^ p.val,
rid2 : ¬M g ^ p ≥ ↑((p.val - 1).fact)
⊢ false
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val,
Hp : (g.nat_degree < p.val ∧ abs (g.coeff 0) < ↑(p.val)) ∧ M g ^ p.val < ↑((p.val - 1).fact)
⊢ p.val > g.nat_degree ∧ p.val > (g.coeff 0).nat_abs
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ M g ≥ 0
exact rid2 rid,
3 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val,
Hp : (g.nat_degree < p.val ∧ abs (g.coeff 0) < ↑(p.val)) ∧ M g ^ p.val < ↑((p.val - 1).fact),
abs_J_lower_bound : ↑((p.val - 1).fact) ≤ abs (J g p.val _),
rid : ↑((p.val - 1).fact) ≤ M g ^ p.val,
rid2 : ¬M g ^ p ≥ ↑((p.val - 1).fact)
⊢ false
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val,
Hp : (g.nat_degree < p.val ∧ abs (g.coeff 0) < ↑(p.val)) ∧ M g ^ p.val < ↑((p.val - 1).fact)
⊢ p.val > g.nat_degree ∧ p.val > (g.coeff 0).nat_abs
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ M g ≥ 0
2 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val,
Hp : (g.nat_degree < p.val ∧ abs (g.coeff 0) < ↑(p.val)) ∧ M g ^ p.val < ↑((p.val - 1).fact)
⊢ p.val > g.nat_degree ∧ p.val > (g.coeff 0).nat_abs
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ M g ≥ 0
assumptions I used in preveious part and lemmas
split,
2 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val,
Hp : (g.nat_degree < p.val ∧ abs (g.coeff 0) < ↑(p.val)) ∧ M g ^ p.val < ↑((p.val - 1).fact)
⊢ p.val > g.nat_degree ∧ p.val > (g.coeff 0).nat_abs
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ M g ≥ 0
3 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val,
Hp : (g.nat_degree < p.val ∧ abs (g.coeff 0) < ↑(p.val)) ∧ M g ^ p.val < ↑((p.val - 1).fact)
⊢ p.val > g.nat_degree
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val,
Hp : (g.nat_degree < p.val ∧ abs (g.coeff 0) < ↑(p.val)) ∧ M g ^ p.val < ↑((p.val - 1).fact)
⊢ p.val > (g.coeff 0).nat_abs
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ M g ≥ 0
exact Hp.1.1,
3 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val,
Hp : (g.nat_degree < p.val ∧ abs (g.coeff 0) < ↑(p.val)) ∧ M g ^ p.val < ↑((p.val - 1).fact)
⊢ p.val > g.nat_degree
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val,
Hp : (g.nat_degree < p.val ∧ abs (g.coeff 0) < ↑(p.val)) ∧ M g ^ p.val < ↑((p.val - 1).fact)
⊢ p.val > (g.coeff 0).nat_abs
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ M g ≥ 0
2 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val,
Hp : (g.nat_degree < p.val ∧ abs (g.coeff 0) < ↑(p.val)) ∧ M g ^ p.val < ↑((p.val - 1).fact)
⊢ p.val > (g.coeff 0).nat_abs
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ M g ≥ 0
have triv := Hp.left.right, rw int.abs_eq_nat_abs at triv, simp only [int.coe_nat_lt] at triv, assumption,
2 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0,
p : nat.primes,
abs_J_upper_bound : abs (J g p.val _) ≤ M g ^ p.val,
Hp : (g.nat_degree < p.val ∧ abs (g.coeff 0) < ↑(p.val)) ∧ M g ^ p.val < ↑((p.val - 1).fact)
⊢ p.val > (g.coeff 0).nat_abs
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ M g ≥ 0
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ M g ≥ 0
rw M, apply mul_nonneg, norm_cast, exact bot_le, apply mul_nonneg, apply mul_nonneg, norm_cast, apply mul_nonneg, exact ge_trans (max_abs_coeff_1_ge_1 g) trivial,
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ M g ≥ 0
3 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ 0 ≤ ↑(g.nat_degree + 1)
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ 0 ≤ real.exp (↑(g.nat_degree) + 1)
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ 0 ≤ (2 * (↑(g.nat_degree) + 1)) ^ (1 + g.nat_degree)
norm_cast, exact bot_le, have triv : (g.nat_degree + 1 : ℝ).exp > 0 := (g.nat_degree + 1:ℝ).exp_pos, exact le_of_lt triv,
3 goals
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ 0 ≤ ↑(g.nat_degree + 1)
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ 0 ≤ real.exp (↑(g.nat_degree) + 1)
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ 0 ≤ (2 * (↑(g.nat_degree) + 1)) ^ (1 + g.nat_degree)
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ 0 ≤ (2 * (↑(g.nat_degree) + 1)) ^ (1 + g.nat_degree)
norm_num, apply pow_nonneg, apply mul_nonneg, linarith, norm_cast, exact bot_le,
g' : ℤ[X],
g'_def : g' ≠ 0 ∧ ⇑(polynomial.aeval e) g' = 0,
g'_nonzero : g' ≠ 0,
e_root_g' : ⇑(polynomial.aeval e) g' = 0,
g : ℤ[X],
g_def : make_const_term_nonzero g' g'_nonzero = g,
coeff_zero_nonzero : g.coeff 0 ≠ 0,
e_root_g : ⇑(polynomial.aeval e) g = 0
⊢ 0 ≤ (2 * (↑(g.nat_degree) + 1)) ^ (1 + g.nat_degree)
no goals