le_normalClosure — Mathlib

English

Let F ⊆ L be fields with K an intermediate field of L containing F. Then K is contained in the normal closure of K in L over F.

Русский

Пусть F ⊆ L — поля, K — промежуточное поле внутри L, содержащее F. Тогда K содержится в нормальном замыкании K внутри L над F.

LaTeX

$$$K \subseteq \operatorname{normalClosure} F K L$$$

Lean4

theorem le_normalClosure : K ≤ normalClosure F K L :=
  K.fieldRange_val.symm.trans_le K.val.fieldRange_le_normalClosure

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