case pos
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
⊢ LinearIndependent K fun i => x ^ ↑i

case neg
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : ¬IsIntegral K x
⊢ LinearIndependent K fun i => x ^ ↑i
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
⊢ LinearIndependent K fun i => x ^ ↑i
by_cases IsIntegral K x
case neg
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : ¬IsIntegral K x
⊢ LinearIndependent K fun i => x ^ ↑i

case pos
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
⊢ LinearIndependent K fun i => x ^ ↑i
case pos
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
⊢ LinearIndependent K fun i => x ^ ↑i

case neg
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : ¬IsIntegral K x
⊢ LinearIndependent K fun i => x ^ ↑i
swap
case pos
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
hg : (Finset.sum Finset.univ fun i => g i • x ^ ↑i) = 0
i : Fin (natDegree (minpoly K x))
⊢ g i = 0
case pos
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
⊢ LinearIndependent K fun i => x ^ ↑i
refine' Fintype.linearIndependent_iff.2 fun g hg i => _
case pos
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
hg : (Finset.sum Finset.univ fun i => g i • x ^ ↑i) = 0
i : Fin (natDegree (minpoly K x))
⊢ g i = 0
case pos
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
hg : (Finset.sum Finset.univ fun i => g i • x ^ ↑i) = 0
i : Fin (natDegree (minpoly K x))
⊢ g i = 0
simp only at hg
case pos
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg : ↑(aeval x) (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = 0
⊢ g i = 0
case pos
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
hg : (Finset.sum Finset.univ fun i => g i • x ^ ↑i) = 0
i : Fin (natDegree (minpoly K x))
⊢ g i = 0
simp_rw [Algebra.smul_def, ← aeval_monomial, ← map_sum] at hg
case pos
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg : ↑(aeval x) (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = 0
⊢ degree (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) < degree (minpoly K x)

R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg : ↑(aeval x) (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = 0
hn0 : ¬g i = 0
h0 : (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = 0
⊢ g i = 0
case pos
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg : ↑(aeval x) (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = 0
⊢ g i = 0
apply (fun hn0 => (minpoly.degree_le_of_ne_zero K x (mt (fun h0 => ?_) hn0) hg).not_lt).mtr
case neg
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : ¬IsIntegral K x
⊢ LinearIndependent K fun i => x ^ ↑i
case neg
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : ¬IsIntegral K x
⊢ LinearIndependent K fun i => x ^ ↑i
rw [minpoly.eq_zero h, natDegree_zero]
no goals
case neg
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : ¬IsIntegral K x
⊢ LinearIndependent K fun i => x ^ ↑i
exact linearIndependent_empty_type
case pos
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg : ↑(aeval x) (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = 0
⊢ degree (Finset.sum Finset.univ fun x_1 => ↑C (g x_1) * X ^ ↑x_1) < degree (minpoly K x)
case pos
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg : ↑(aeval x) (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = 0
⊢ degree (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) < degree (minpoly K x)
simp_rw [← C_mul_X_pow_eq_monomial]
no goals
case pos
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg : ↑(aeval x) (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = 0
⊢ degree (Finset.sum Finset.univ fun x_1 => ↑C (g x_1) * X ^ ↑x_1) < degree (minpoly K x)
exact (degree_eq_natDegree <| minpoly.ne_zero h).symm ▸ degree_sum_fin_lt _
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg : ↑(aeval x) (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = 0
hn0 : ¬g i = 0
h0 : ↑(lcoeff K ↑i) (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = ↑(lcoeff K ↑i) 0
⊢ g i = 0
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg : ↑(aeval x) (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = 0
hn0 : ¬g i = 0
h0 : (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = 0
⊢ g i = 0
apply_fun lcoeff K i at h0
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg : ↑(aeval x) (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = 0
hn0 : ¬g i = 0
h0 : (if i ∈ Finset.univ then g i else 0) = coeff 0 ↑i
⊢ g i = 0
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg : ↑(aeval x) (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = 0
hn0 : ¬g i = 0
h0 : ↑(lcoeff K ↑i) (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = ↑(lcoeff K ↑i) 0
⊢ g i = 0
simp_rw [map_sum, lcoeff_apply, coeff_monomial, Fin.val_eq_val, Finset.sum_ite_eq'] at h0
no goals
R : Type ?u.641649
S : Type u_2
T : Type ?u.641655
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type ?u.641958
B : Type ?u.641961
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg : ↑(aeval x) (Finset.sum Finset.univ fun x_1 => ↑(monomial ↑x_1) (g x_1)) = 0
hn0 : ¬g i = 0
h0 : (if i ∈ Finset.univ then g i else 0) = coeff 0 ↑i
⊢ g i = 0
exact (if_pos <| Finset.mem_univ _).symm.trans h0