normal_iff_normalClosure_eq — Mathlib

English

A field K is normal over F if and only if its normal closure in L over F equals K.

Русский

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

LaTeX

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

Lean4

theorem normal_iff_normalClosure_eq : Normal F K ↔ normalClosure F K L = K :=
  ⟨@normalClosure_of_normal (K := K), fun h ↦ h ▸ normalClosure.normal F K L⟩

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