normal_iff_normalClosure_le

Mathlib.FieldTheory.Normal.Closure

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

← MathLib Explorer

English

A field K is normal over F if and only if normalClosure F K L ≤ K.

Русский

Поле K нормально над F тогда и только тогда, когда normalClosure F K L ≤ K.

LaTeX

$$$\mathrm{Normal} F K \iff \operatorname{normalClosure} F K L \le K$$$

Lean4

theorem normal_iff_normalClosure_le : Normal F K ↔ normalClosure F K L ≤ K :=
  normal_iff_normalClosure_eq.trans (le_normalClosure K).ge_iff_eq'.symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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