separable — Mathlib

English

In characteristic zero, every irreducible polynomial over a field F is separable.

Русский

В характеристике ноль над полем F каждый неприводимый полином является разделяемым.

LaTeX

$$[CharZero F] Irreducible f ⇒ f.Separable$$

Lean4

theorem _root_.Irreducible.separable [CharZero F] {f : F[X]} (hf : Irreducible f) : f.Separable :=
  by
  rw [separable_iff_derivative_ne_zero hf, Ne, ← degree_eq_bot, degree_derivative_eq]
  · rintro ⟨⟩
  exact Irreducible.natDegree_pos hf

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