normal_iff_forall_fieldRange_le — Mathlib

English

A field K is normal over F if and only if for every F-algebra homomorphism σ: K → L, the fieldRange of σ is contained in K.

Русский

Поле K нормально над F тогда и только тогда, когда для каждого гомоморфизма F-алгебр σ: K → L, полеобраз σ лежит в K.

LaTeX

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

Lean4

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

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