R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q : ℕ
p : R[X]
hsep : Separable p
⊢ ∀ (x : R[X]), multiplicity x p ≤ 1 ∨ IsUnit x
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q : ℕ
p : R[X]
hsep : Separable p
⊢ Squarefree p
rw [multiplicity.squarefree_iff_multiplicity_le_one p]
no goals
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q : ℕ
p : R[X]
hsep : Separable p
⊢ ∀ (x : R[X]), multiplicity x p ≤ 1 ∨ IsUnit x
exact fun f => or_iff_not_imp_right.mpr fun hunit => multiplicity_le_one_of_separable hunit hsep