normalClosure_def — Mathlib

English

The normal closure of K/F in L is the supremum of the ranges of all F-algebra homomorphisms from K to L.

Русский

Нормальное замыкание K/F в L равно наибольшему по включению из всех образов K в L под F-алгебраическими гомоморфизмами.

LaTeX

$$$\operatorname{normalClosure}(F,K,L)=\bigvee_{f:K\to_{F}L} f.fieldRange$$$

Lean4

theorem normalClosure_def : normalClosure F K L = ⨆ f : K →ₐ[F] L, f.fieldRange :=
  rfl

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