isSeparable_iff — Mathlib

English

An extension F ⊆ K is separable if and only if every element of K is integral and separable over F.

Русский

Расщепление F ⊆ K эквивалентно тому, что каждый элемент K интеграл и разделяем над F.

LaTeX

$$Algebra.IsSeparable F K ↔ ∀ x : K, IsIntegral F x ∧ IsSeparable F x$$

Lean4

theorem isSeparable_iff : Algebra.IsSeparable F K ↔ ∀ x : K, IsIntegral F x ∧ IsSeparable F x :=
  ⟨fun _ x => ⟨Algebra.IsSeparable.isIntegral F x, Algebra.IsSeparable.isSeparable F x⟩, fun h => ⟨fun x => (h x).2⟩⟩

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