numberField — Mathlib

English

If S is finite and IsCyclotomicExtension S K C, then FiniteDimensional K C.

Русский

Если S конечное и IsCyclotomicExtension S K C, то C является конечнодименсиональным над K.

LaTeX

$$$[Finite S] \\Rightarrow [IsCyclotomicExtension S K C] \\Rightarrow FiniteDimensional K C$$$

Lean4

/-- A cyclotomic finite extension of a number field is a number field. -/
theorem numberField [h : NumberField K] [Finite S] [IsCyclotomicExtension S K L] : NumberField L :=
  { to_charZero := charZero_of_injective_algebraMap (algebraMap K L).injective
    to_finiteDimensional :=
      by
      haveI := charZero_of_injective_algebraMap (algebraMap K L).injective
      haveI := IsCyclotomicExtension.finite S K L
      exact Module.Finite.trans K _ }

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