eq_top_iff — Mathlib

English

The separable closure of F in E equals the top (i.e., E) if and only if E/F is separable.

Русский

Замыкание по сепарабельности F в E равно верхнему элементу (то есть E) тогда и только тогда, когда E/F сепарабельно.

LaTeX

$$$\\mathrm{separableClosure}(F,E) = \\top \\iff \\mathrm{Algebra.IsSeparable}\nF E$$$

Lean4

/-- The separable closure of `F` in `E` is equal to `E` if and only if `E / F` is
separable. -/
theorem eq_top_iff : separableClosure F E = ⊤ ↔ Algebra.IsSeparable F E :=
  ⟨fun h ↦ ⟨fun _ ↦ mem_separableClosure_iff.1 (h ▸ mem_top)⟩, fun _ ↦
    top_unique fun x _ ↦ mem_separableClosure_iff.2 (Algebra.IsSeparable.isSeparable _ x)⟩

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