of_subfield

Mathlib.NumberTheory.NumberField.Basic

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

English

If E is a subfield of K, then E is a number field.

Русский

Если E является подполем K, то E — число поле.

LaTeX

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

Lean4

instance of_subfield [NumberField K] (E : Subfield K) : NumberField E where
  to_finiteDimensional := FiniteDimensional.left ℚ E K

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

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

Разделы

Аффилиация

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