normal_iff_forall_map_le — Mathlib

English

A field K is normal over F if and only if for every endomorphism σ: L →ₐ[F] L, the fieldRange of σ restricted to K is contained in K.

Русский

Поле K нормально над F тогда и только тогда, когда для каждого эндоморфизма σ: L →ₐ[F] L полеобраз σ(K) ⊆ K.

LaTeX

$$$\mathrm{Normal} F K \iff \forall \sigma : L \to_{F} L, \sigma(\mathrm{fieldRange}) \le K$$$

Lean4

theorem normal_iff_forall_map_le : Normal F K ↔ ∀ σ : L →ₐ[F] L, K.map σ ≤ K := by
  rw [normal_iff_normalClosure_le, normalClosure_def', iSup_le_iff]

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