isSepClosure_iff — Mathlib

English

For fields k, K with k-algebra structure, IsSepClosure k K is equivalent to IsSepClosed K together with Algebra.IsSeparable k K.

Русский

Для полей k, K с k-алгебрическим строем IsSepClosure k K эквивалентно IsSepClosed K и Algebra.IsSeparable k K.

LaTeX

$$IsSepClosure k K ↔ IsSepClosed K ∧ Algebra.IsSeparable k K$$

Lean4

theorem isSepClosure_iff [Algebra k K] : IsSepClosure k K ↔ IsSepClosed K ∧ Algebra.IsSeparable k K :=
  ⟨fun h ↦ ⟨h.1, h.2⟩, fun h ↦ ⟨h.1, h.2⟩⟩

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