isSeparable_sup — Mathlib

English

A compositum (supremum) of a family of separable extensions is separable.

Русский

Объединение (супремум) семейства сепарабельных расширений является сепарабельным.

LaTeX

$$$\\bigl(\\forall i, \\text{Algebra.IsSeparable } F (t_i)\\bigr) \\Rightarrow \\text{Algebra.IsSeparable } F (\\bigsqcup_i t_i)$$$

Lean4

/-- A compositum of two separable extensions is separable. -/
instance isSeparable_sup (L1 L2 : IntermediateField F E) [h1 : Algebra.IsSeparable F L1]
    [h2 : Algebra.IsSeparable F L2] : Algebra.IsSeparable F (L1 ⊔ L2 : IntermediateField F E) :=
  by
  rw [← le_separableClosure_iff] at h1 h2 ⊢
  exact sup_le h1 h2

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