eq_bot_of_isPurelyInseparable — Mathlib

English

If E/F is purely inseparable, then the separable closure of F in E is F itself.

Русский

Если расширение E/F чисто безразделимо, то сепарабельное замыкание F в E равно F.

LaTeX

$$separableClosure F E = ⊥$$

Lean4

/-- If `E / F` is purely inseparable, then the separable closure of `F` in `E` is
equal to `F`. -/
theorem eq_bot_of_isPurelyInseparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E]
    [IsPurelyInseparable F E] : separableClosure F E = ⊥ :=
  bot_unique fun x h ↦ IsPurelyInseparable.inseparable F x (mem_separableClosure_iff.1 h)

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