not_irreducible_expand — 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

@[simp]
theorem not_irreducible_expand (R p) [CommSemiring R] [Fact p.Prime] [CharP R p] [PerfectRing R p] (f : R[X]) :
    ¬Irreducible (expand R p f) := by
  rw [polynomial_expand_eq]
  exact not_irreducible_pow (Fact.out : p.Prime).ne_one

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