R : Type ?u.115843
S : Type u_2
T : Type ?u.115849
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.116155
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.116577
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : ↑(aeval pb.gen) p = 0
hlt : natDegree p < pb.dim
⊢ p = 0
R : Type ?u.115843
S : Type u_2
T : Type ?u.115849
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.116155
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.116577
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : ↑(aeval pb.gen) p = 0
⊢ pb.dim ≤ natDegree p
refine' le_of_not_lt fun hlt => ne_zero _
R : Type ?u.115843
S : Type u_2
T : Type ?u.115849
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.116155
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.116577
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : ↑(aeval pb.gen) p = 0
hlt : natDegree p < pb.dim
⊢ ∑ i : Fin pb.dim, ↑(monomial ↑i) (coeff p ↑i) = 0
R : Type ?u.115843
S : Type u_2
T : Type ?u.115849
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.116155
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.116577
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : ↑(aeval pb.gen) p = 0
hlt : natDegree p < pb.dim
⊢ p = 0
rw [p.as_sum_range' _ hlt, Finset.sum_range]
R : Type ?u.115843
S : Type u_2
T : Type ?u.115849
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.116155
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.116577
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : ↑(aeval pb.gen) p = 0
hlt : natDegree p < pb.dim
i : Fin pb.dim
⊢ ↑(monomial ↑i) (coeff p ↑i) = 0
R : Type ?u.115843
S : Type u_2
T : Type ?u.115849
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.116155
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.116577
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : ↑(aeval pb.gen) p = 0
hlt : natDegree p < pb.dim
⊢ ∑ i : Fin pb.dim, ↑(monomial ↑i) (coeff p ↑i) = 0
refine' Fintype.sum_eq_zero _ fun i => _
R : Type ?u.115843
S : Type u_2
T : Type ?u.115849
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.116155
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.116577
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
hlt : natDegree p < pb.dim
i : Fin pb.dim
root : ∑ x : Fin pb.dim, coeff p ↑x • ↑pb.basis x = 0
⊢ ↑(monomial ↑i) (coeff p ↑i) = 0
R : Type ?u.115843
S : Type u_2
T : Type ?u.115849
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.116155
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.116577
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : ↑(aeval pb.gen) p = 0
hlt : natDegree p < pb.dim
i : Fin pb.dim
⊢ ↑(monomial ↑i) (coeff p ↑i) = 0
simp_rw [aeval_eq_sum_range' hlt, Finset.sum_range, ← pb.basis_eq_pow] at root
R : Type ?u.115843
S : Type u_2
T : Type ?u.115849
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.116155
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.116577
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
hlt : natDegree p < pb.dim
i : Fin pb.dim
root : ∑ x : Fin pb.dim, coeff p ↑x • ↑pb.basis x = 0
this : ∀ (i : Fin pb.dim), coeff p ↑i = 0
⊢ ↑(monomial ↑i) (coeff p ↑i) = 0
R : Type ?u.115843
S : Type u_2
T : Type ?u.115849
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.116155
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.116577
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
hlt : natDegree p < pb.dim
i : Fin pb.dim
root : ∑ x : Fin pb.dim, coeff p ↑x • ↑pb.basis x = 0
⊢ ↑(monomial ↑i) (coeff p ↑i) = 0
have := Fintype.linearIndependent_iff.1 pb.basis.linearIndependent _ root
R : Type ?u.115843
S : Type u_2
T : Type ?u.115849
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.116155
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.116577
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
hlt : natDegree p < pb.dim
i : Fin pb.dim
root : ∑ x : Fin pb.dim, coeff p ↑x • ↑pb.basis x = 0
this : ∀ (i : Fin pb.dim), coeff p ↑i = 0
⊢ ↑(monomial ↑i) (coeff p ↑i) = 0
R : Type ?u.115843
S : Type u_2
T : Type ?u.115849
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.116155
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.116577
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
hlt : natDegree p < pb.dim
i : Fin pb.dim
root : ∑ x : Fin pb.dim, coeff p ↑x • ↑pb.basis x = 0
this : ∀ (i : Fin pb.dim), coeff p ↑i = 0
⊢ ↑(monomial ↑i) (coeff p ↑i) = 0
dsimp only at this
no goals
R : Type ?u.115843
S : Type u_2
T : Type ?u.115849
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.116155
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.116577
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
hlt : natDegree p < pb.dim
i : Fin pb.dim
root : ∑ x : Fin pb.dim, coeff p ↑x • ↑pb.basis x = 0
this : ∀ (i : Fin pb.dim), coeff p ↑i = 0
⊢ ↑(monomial ↑i) (coeff p ↑i) = 0
rw [this, monomial_zero_right]