no goals
R : Type ?u.140709
S : Type u_2
T : Type ?u.140715
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_1
B : Type ?u.141021
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra A B
K : Type ?u.141443
inst✝² : Field K
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ degree (minpoly A pb.gen) = ↑pb.dim
rw [← minpolyGen_eq, degree_minpolyGen]