isSeparable_adjoin_iff_isSeparable

English

A field extension F(S)/F is separable if and only if every element of S is separable over F.

Русский

Расширение F(S)/F является сепарабельным тогда и только тогда, когда каждый элемент S сепарабелен над F.

LaTeX

$$$\\mathrm{IsSeparable}_F(\\mathrm{adjoin}(F,S)) \\iff \\forall x\\in S,\\ IsSeparable_F(x)$$$

Lean4

/-- `F(S) / F` is a separable extension if and only if all elements of `S` are
separable elements. -/
theorem isSeparable_adjoin_iff_isSeparable {S : Set E} :
    Algebra.IsSeparable F (adjoin F S) ↔ ∀ x ∈ S, IsSeparable F x :=
  (le_separableClosure_iff F E _).symm.trans adjoin_le_iff

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