splits_of_natSepDegree_eq_one — Mathlib

English

A field is perfect if and only if every separable degree one polynomial splits.

Русский

Поле идеальное тогда и только тогда, когда любой полином степени сепарабельности 1 распадается на множители.

LaTeX

$$$ PerfectField F \iff \forall f : F[X], f.natSepDegree = 1 \to f.Splits (RingHom.id F) $$$

Lean4

theorem splits_of_natSepDegree_eq_one [PerfectField K] {f : E[X]} (i : E →+* K) (hf : f.natSepDegree = 1) :
    f.Splits i :=
  (splits_id_iff_splits _).mp <|
    (perfectField_iff_splits_of_natSepDegree_eq_one K).mp ‹_› _ (natSepDegree_map K f i ▸ hf)

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