case a
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
r s : R
⊢ count s (roots (X - ↑C r)) = count s {r}
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
r : R
⊢ roots (X - ↑C r) = {r}
ext s
no goals
case a
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
r s : R
⊢ count s (roots (X - ↑C r)) = count s {r}
rw [count_roots, rootMultiplicity_X_sub_C, count_singleton]