case a
R : Type u_1
A : Type ?u.886014
B : Type ?u.886017
S : Type ?u.886020
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
p : R[X]
x : S
⊢ degree (normalizeScaleRoots p) ≤ degree p

case a
R : Type u_1
A : Type ?u.886014
B : Type ?u.886017
S : Type ?u.886020
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
p : R[X]
x : S
⊢ degree p ≤ degree (normalizeScaleRoots p)
R : Type u_1
A : Type ?u.886014
B : Type ?u.886017
S : Type ?u.886020
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
p : R[X]
x : S
⊢ degree (normalizeScaleRoots p) = degree p
apply le_antisymm
no goals
case a
R : Type u_1
A : Type ?u.886014
B : Type ?u.886017
S : Type ?u.886020
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
p : R[X]
x : S
⊢ degree (normalizeScaleRoots p) ≤ degree p
exact Finset.sup_mono (normalizeScaleRoots_support p)
case a
R : Type u_1
A : Type ?u.886014
B : Type ?u.886017
S : Type ?u.886020
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
p : R[X]
x : S
⊢ degree (leadingCoeff p • normalizeScaleRoots p) ≤ degree (normalizeScaleRoots p)
case a
R : Type u_1
A : Type ?u.886014
B : Type ?u.886017
S : Type ?u.886020
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
p : R[X]
x : S
⊢ degree p ≤ degree (normalizeScaleRoots p)
rw [← degree_scaleRoots, ← leadingCoeff_smul_normalizeScaleRoots]
no goals
case a
R : Type u_1
A : Type ?u.886014
B : Type ?u.886017
S : Type ?u.886020
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
p : R[X]
x : S
⊢ degree (leadingCoeff p • normalizeScaleRoots p) ≤ degree (normalizeScaleRoots p)
exact degree_smul_le _ _