squarefree — Mathlib

English

A separable polynomial is squarefree.

Русский

Разделимый многочлен квадратно свободен.

LaTeX

$$$\\operatorname{Separable}(p) \\Rightarrow \\operatorname{Squarefree}(p)$$$

Lean4

/-- A separable polynomial is square-free.

See `PerfectField.separable_iff_squarefree` for the converse when the coefficients are a perfect
field. -/
theorem squarefree {p : R[X]} (hsep : Separable p) : Squarefree p := by
  classical
  rw [squarefree_iff_emultiplicity_le_one p]
  exact fun f => or_iff_not_imp_right.mpr fun hunit => emultiplicity_le_one_of_separable hunit hsep

Похожие утверждения