normalClosure_of_normal

Mathlib.FieldTheory.Normal.Closure

URI: https://scilib.ai/kg/mathlib#IntermediateField.normalClosure_of_normal

English

If K is normal over F, then the normal closure of K in L over F is K itself.

Русский

Если K нормально над F, то нормальное замыкание K в L над F равно самому K.

LaTeX

$$$\operatorname{normalClosure} F K L = K\quad\text{whenever } \mathrm{Normal} F K$$$

Lean4

theorem normalClosure_of_normal [Normal F K] : normalClosure F K L = K := by
  simp only [normalClosure_def, AlgHom.fieldRange_of_normal, iSup_const]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru