R : Type ?u.111432
S : Type u_2
T : Type ?u.111438
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.111744
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.112166
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
✝ : Nontrivial A
⊢ Monic (minpolyGen pb)
R : Type ?u.111432
S : Type u_2
T : Type ?u.111438
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.111744
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.112166
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ Monic (minpolyGen pb)
nontriviality A
R : Type ?u.111432
S : Type u_2
T : Type ?u.111438
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.111744
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.112166
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
✝ : Nontrivial A
⊢ degree (∑ i : Fin pb.dim, ↑C (↑(↑pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i) < degree (X ^ pb.dim)
R : Type ?u.111432
S : Type u_2
T : Type ?u.111438
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.111744
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.112166
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
✝ : Nontrivial A
⊢ Monic (minpolyGen pb)
apply (monic_X_pow _).sub_of_left _
R : Type ?u.111432
S : Type u_2
T : Type ?u.111438
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.111744
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.112166
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
✝ : Nontrivial A
⊢ degree (∑ i : Fin pb.dim, ↑C (↑(↑pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i) < ↑pb.dim
R : Type ?u.111432
S : Type u_2
T : Type ?u.111438
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.111744
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.112166
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
✝ : Nontrivial A
⊢ degree (∑ i : Fin pb.dim, ↑C (↑(↑pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i) < degree (X ^ pb.dim)
rw [degree_X_pow]
no goals
R : Type ?u.111432
S : Type u_2
T : Type ?u.111438
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.111744
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.112166
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
✝ : Nontrivial A
⊢ degree (∑ i : Fin pb.dim, ↑C (↑(↑pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i) < ↑pb.dim
exact degree_sum_fin_lt _