case pos
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
h : IsRoot p t
⊢ rootMultiplicity t p - 1 ≤ rootMultiplicity t (↑derivative p)

case neg
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
h : ¬IsRoot p t
⊢ rootMultiplicity t p - 1 ≤ rootMultiplicity t (↑derivative p)
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
⊢ rootMultiplicity t p - 1 ≤ rootMultiplicity t (↑derivative p)
by_cases p.IsRoot t
no goals
case pos
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
h : IsRoot p t
⊢ rootMultiplicity t p - 1 ≤ rootMultiplicity t (↑derivative p)
exact (derivative_rootMultiplicity_of_root h).symm.le
case neg
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
h : ¬IsRoot p t
⊢ 0 ≤ rootMultiplicity t (↑derivative p)
case neg
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
h : ¬IsRoot p t
⊢ rootMultiplicity t p - 1 ≤ rootMultiplicity t (↑derivative p)
rw [rootMultiplicity_eq_zero h, zero_tsub]
no goals
case neg
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
h : ¬IsRoot p t
⊢ 0 ≤ rootMultiplicity t (↑derivative p)
exact zero_le _