R : Type ?u.124871
S : Type u_2
T : Type ?u.124877
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.125183
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.125605
inst✝¹ : Field K
inst✝ : Algebra A S
h : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : ↑(aeval h.gen) p = 0
⊢ ↑h.dim ≤ ↑(natDegree p)
R : Type ?u.124871
S : Type u_2
T : Type ?u.124877
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.125183
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.125605
inst✝¹ : Field K
inst✝ : Algebra A S
h : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : ↑(aeval h.gen) p = 0
⊢ ↑h.dim ≤ degree p
rw [degree_eq_natDegree ne_zero]
no goals
R : Type ?u.124871
S : Type u_2
T : Type ?u.124877
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.125183
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.125605
inst✝¹ : Field K
inst✝ : Algebra A S
h : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : ↑(aeval h.gen) p = 0
⊢ ↑h.dim ≤ ↑(natDegree p)
exact WithBot.coe_le_coe.2 (h.dim_le_natDegree_of_root ne_zero root)