normal_iff_forall_map_le' — Mathlib

English

A field K is normal over F iff for all endomorphisms σ: L →ₐ[F] L, the fieldRange of σ applied to K equals K.

Русский

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

LaTeX

$$$\mathrm{Normal} F K \iff \forall \sigma : L \to_{F} L, \sigma( K ) = 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]

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