finiteDimensional — Mathlib

English

For S finite and IsCyclotomicExtension S K C, FiniteDimensional K C.

Русский

Для конечного S и IsCyclotomicExtension S K C верно FiniteDimensional K C.

LaTeX

$$$IsCyclotomicExtension S K C \\Rightarrow FiniteDimensional K C$ (при условии конечности S).$$

Lean4

/-- If `S` is finite and `IsCyclotomicExtension S K A`, then `finiteDimensional K A`. -/
theorem finiteDimensional (C : Type z) [Finite S] [CommRing C] [Algebra K C] [IsDomain C]
    [IsCyclotomicExtension S K C] : FiniteDimensional K C :=
  IsCyclotomicExtension.finite S K C

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