isAlgebraic

Mathlib.NumberTheory.NumberField.Basic

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

English

If K is a number field, then K is algebraic over Q.

Русский

Если K — число поле, то K алгебраически расширено над \\math{Q}.

LaTeX

$$$$ \\text{Algebraic}_{\\mathbb{Q}}(K) $$$$

Lean4

protected theorem isAlgebraic [NumberField K] : Algebra.IsAlgebraic ℚ K :=
  Algebra.IsAlgebraic.of_finite _ _

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

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

Разделы

Аффилиация

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