separable_iff_squarefree — Mathlib

English

Over a perfect field K, a polynomial g ∈ K[X] is separable if and only if it is squarefree.

Русский

Над совершенным полем K многочлен g ∈ K[X] разделим тогда и только тогда, когда он квадратно-разложим (squarefree).

LaTeX

$$$ g\text{ Separable} \iff g\text{ Squarefree}. $$$

Lean4

theorem separable_iff_squarefree {g : K[X]} : g.Separable ↔ Squarefree g :=
  by
  refine ⟨Separable.squarefree, fun sqf ↦ isCoprime_of_irreducible_dvd (sqf.ne_zero ·.1) ?_⟩
  rintro p (h : Irreducible p) ⟨q, rfl⟩ (dvd : p ∣ derivative (p * q))
  replace dvd : p ∣ q := by
    rw [derivative_mul, dvd_add_left (dvd_mul_right p _)] at dvd
    exact (separable_of_irreducible h).dvd_of_dvd_mul_left dvd
  exact (h.1 : ¬IsUnit p) (sqf _ <| mul_dvd_mul_left _ dvd)

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