R : Type ?u.130887
S : Type u_2
T : Type ?u.130893
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_1
B : Type ?u.131199
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra A B
K : Type ?u.131621
inst✝² : Field K
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ degree (X ^ pb.dim - ∑ i : Fin pb.dim, ↑C (↑(↑pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i) = ↑pb.dim
R : Type ?u.130887
S : Type u_2
T : Type ?u.130893
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_1
B : Type ?u.131199
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra A B
K : Type ?u.131621
inst✝² : Field K
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ degree (minpolyGen pb) = ↑pb.dim
unfold minpolyGen
R : Type ?u.130887
S : Type u_2
T : Type ?u.130893
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_1
B : Type ?u.131199
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra A B
K : Type ?u.131621
inst✝² : Field K
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ degree (∑ i : Fin pb.dim, ↑C (↑(↑pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i) < ↑pb.dim
R : Type ?u.130887
S : Type u_2
T : Type ?u.130893
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_1
B : Type ?u.131199
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra A B
K : Type ?u.131621
inst✝² : Field K
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ degree (X ^ pb.dim - ∑ i : Fin pb.dim, ↑C (↑(↑pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i) = ↑pb.dim
rw [degree_sub_eq_left_of_degree_lt] <;> rw [degree_X_pow]
no goals
R : Type ?u.130887
S : Type u_2
T : Type ?u.130893
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_1
B : Type ?u.131199
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra A B
K : Type ?u.131621
inst✝² : Field K
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ degree (∑ i : Fin pb.dim, ↑C (↑(↑pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i) < ↑pb.dim
apply degree_sum_fin_lt