normal — Mathlib

English

A purely inseparable extension is normal.

Русский

Чисто бесприводное расширение нормальное.

LaTeX

$$$\text{Normal } F E$$$

Lean4

/-- A purely inseparable extension is normal. -/
instance normal [IsPurelyInseparable F E] : Normal F E
    where
  toIsAlgebraic := isAlgebraic F E
  splits'
    x := by
    obtain ⟨n, h⟩ := IsPurelyInseparable.minpoly_eq_X_sub_C_pow F (ringExpChar F) x
    rw [← splits_id_iff_splits, h]
    exact splits_pow _ (splits_X_sub_C _) _

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