R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hsep : Separable p
x : R
⊢ rootMultiplicity x p ≤ 1
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hsep : Separable p
x : R
⊢ Multiset.count x (roots p) ≤ 1
rw [count_roots p]
no goals
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hsep : Separable p
x : R
⊢ rootMultiplicity x p ≤ 1
exact rootMultiplicity_le_one_of_separable hsep x