finiteDimensional — Mathlib

English

If f has IsSplittingField over L with K-algebra structure, then L is finite-dimensional over K.

Русский

Если f имеет IsSplittingField над L с K-алгеброй, то L конечно по размерности над K.

LaTeX

$$$\text{FiniteDimensional } K L$$$

Lean4

theorem finiteDimensional (f : K[X]) [IsSplittingField K L f] : FiniteDimensional K L := by
  classical
    exact
    ⟨@Algebra.top_toSubmodule K L _ _ _ ▸
        adjoin_rootSet L f ▸
          fg_adjoin_of_finite (Finset.finite_toSet _) fun y hy ↦
            if hf : f = 0 then by rw [hf, rootSet_zero] at hy; cases hy
            else IsAlgebraic.isIntegral ⟨f, hf, (mem_rootSet'.mp hy).2⟩⟩

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