of_intermediateField

Mathlib.NumberTheory.NumberField.Basic

URI: https://scilib.ai/kg/mathlib#NumberField.of_intermediateField

English

If E is an intermediate field between K and L, then E is a number field.

Русский

Если E является промежуточным полем между K и L, то E — число поле.

LaTeX

$$$$ NumberField(E) $$$$

Lean4

instance of_intermediateField [NumberField K] [NumberField L] [Algebra K L] (E : IntermediateField K L) :
    NumberField E :=
  of_module_finite K E

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru