normal — Mathlib

English

If K is finite-dimensional over F, then the normalClosure F K L is finite-dimensional over F.

Русский

Если K/ F конечно размерно, то normalClosure F K L размерно над F.

LaTeX

$$$\text{FiniteDimensional}_F(K) \Rightarrow \text{FiniteDimensional}_F(\operatorname{normalClosure}(F,K,L))$$$

Lean4

@[stacks 0BMG "(1) normality."]
instance normal [h : Normal F L] : Normal F (normalClosure F K L) :=
  by
  obtain _ | φ := isEmpty_or_nonempty (K →ₐ[F] L)
  · rw [normalClosure, iSup_of_empty]; exact Normal.of_algEquiv (botEquiv F L).symm
  · exact (isNormalClosure_normalClosure F K L).normal

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