normalClosure_le_iff — Mathlib

English

For intermediate field K' between F and L, normalClosure F K L ≤ K' if and only if every F-algebra hom f: K → L has its field range contained in K'.

Русский

Для промежуточного поля K' между F и L выполняется: нормальная замкнутость F K L меньше или равна K' тогда и только тогда, когда для каждого F-алгоморафизма f: K → L область значений лежит в K'.

LaTeX

$$$\text{normalClosure } F K L \leq K' \iff \forall f : K \to_{F} L, f.fieldRange \leq K'$$$

Lean4

theorem normalClosure_le_iff {K' : IntermediateField F L} :
    normalClosure F K L ≤ K' ↔ ∀ f : K →ₐ[F] L, f.fieldRange ≤ K' :=
  iSup_le_iff

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