F : Type ?u.870038
inst✝⁶ : Field F
E : Type ?u.870044
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
α : E
K : Type u_1
inst✝³ : Field K
inst✝² : Algebra F K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ (powerBasis hx).dim = natDegree (minpoly K x)
F : Type ?u.870038
inst✝⁶ : Field F
E : Type ?u.870044
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
α : E
K : Type u_1
inst✝³ : Field K
inst✝² : Algebra F K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ FiniteDimensional.finrank K { x_1 // x_1 ∈ K⟮x⟯ } = natDegree (minpoly K x)
rw [PowerBasis.finrank (adjoin.powerBasis hx : _)]
no goals
F : Type ?u.870038
inst✝⁶ : Field F
E : Type ?u.870044
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
α : E
K : Type u_1
inst✝³ : Field K
inst✝² : Algebra F K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ (powerBasis hx).dim = natDegree (minpoly K x)
rfl