is_finiteDimensional — Mathlib

English

There is a canonical IsScalarTower structure between F, K, and the normalClosure F K L, making the scalar actions compatible.

Русский

Существует каноническая структура IsScalarTower между F, K и normalClosure F K L, обеспечивающая совместимость действия скаляров.

LaTeX

$$$\text{IsScalarTower } F\ K\ (\operatorname{normalClosure}(F,K,L))$$$

Lean4

@[stacks 0BMG "When `L` is normal over `K`, this agrees with 0BMG (1) finiteness."]
instance is_finiteDimensional [FiniteDimensional F K] : FiniteDimensional F (normalClosure F K L) :=
  by
  haveI : ∀ f : K →ₐ[F] L, FiniteDimensional F f.fieldRange := fun f ↦ f.toLinearMap.finiteDimensional_range
  apply IntermediateField.finiteDimensional_iSup_of_finite

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