adjoin_le — Mathlib

English

In a tower E/F/K, adjoin E (separableClosure F K) is contained in separableClosure E K.

Русский

В башне E/F/K adjoin E (separableClosure F K) содержится в separableClosure E K.

LaTeX

$$$\\mathrm{adjoin}_E(\\mathrm{separableClosure}(F,K)) \\le \\mathrm{separableClosure}(E,K)$$$

Lean4

/-- If `K / E / F` is a field extension tower, then `E` adjoin `separableClosure F K` is contained
in `separableClosure E K`. -/
theorem adjoin_le [Algebra E K] [IsScalarTower F E K] : adjoin E (separableClosure F K) ≤ separableClosure E K :=
  adjoin_le_iff.2 <| le_restrictScalars F E K

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