case inl
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x y : R
hxy : x = y
⊢ rootMultiplicity x (X - ↑C y) = 1

case inr
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x y : R
hxy : ¬x = y
⊢ rootMultiplicity x (X - ↑C y) = 0
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x y : R
⊢ rootMultiplicity x (X - ↑C y) = if x = y then 1 else 0
split_ifs with hxy
no goals
case inr
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x y : R
hxy : ¬x = y
⊢ rootMultiplicity x (X - ↑C y) = 0
exact rootMultiplicity_eq_zero (mt root_X_sub_C.mp (Ne.symm hxy))
case inl
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x y : R
hxy : x = y
⊢ rootMultiplicity y (X - ↑C y) = 1
case inl
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x y : R
hxy : x = y
⊢ rootMultiplicity x (X - ↑C y) = 1
rw [hxy]
no goals
case inl
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x y : R
hxy : x = y
⊢ rootMultiplicity y (X - ↑C y) = 1
exact rootMultiplicity_X_sub_C_self