instFreeInt

Mathlib.NumberTheory.NumberField.Basic

URI: https://scilib.ai/kg/mathlib#NumberField.RingOfIntegers.instFreeInt

English

𝓞_K is a free ℤ-module.

Русский

𝓞_K является свободным ℤ-модулем.

LaTeX

$$$\\mathcal{O}_K\\ \\text{is a free } \\mathbb{Z}-\\text{module}$$$

Lean4

instance : Free ℤ (𝓞 K) :=
  IsIntegralClosure.module_free ℤ ℚ K (𝓞 K)

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

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

Разделы

Аффилиация

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