of_module_finite — Mathlib

English

A finite extension of a number field is a number field.

Русский

Конечное расширение числа поля является числовым полем.

LaTeX

$$$$ NumberField(L) $$$$

Lean4

/-- A finite extension of a number field is a number field. -/
theorem of_module_finite [NumberField K] [Algebra K L] [Module.Finite K L] : NumberField L
    where
  to_charZero := charZero_of_injective_algebraMap (algebraMap K L).injective
  to_finiteDimensional :=
    letI := charZero_of_injective_algebraMap (algebraMap K L).injective
    Module.Finite.trans K L

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