isPurelyInseparable_iff — Mathlib

English

The property IsPurelyInseparable F E is equivalent to: every x is integral over F and whenever x is separable over F, then x lies in the range of F in E.

Русский

Свойство IsPurelyInseparable F E эквивалентно: каждый элемент интегрален над F, и если элемент разделяем над F, то он лежит в образе F в E.

LaTeX

$$$IsPurelyInseparable F E\iff \forall x\in E,\ IsIntegral F x\land (IsSeparable F x \to x\in (algebraMap F E).range)$$$

Lean4

theorem isPurelyInseparable_iff :
    IsPurelyInseparable F E ↔ ∀ x : E, IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range) :=
  ⟨fun h x ↦ ⟨h.isIntegral' _ x, h.inseparable' x⟩, fun h ↦ ⟨⟨fun x ↦ (h x).1⟩, fun x ↦ (h x).2⟩⟩

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