ringOfIntegersEquiv

Mathlib.NumberTheory.NumberField.Basic

URI: https://scilib.ai/kg/mathlib#Rat.ringOfIntegersEquiv

English

The ring of integers of ℚ is naturally identified with ℤ; they are isomorphic as rings.

Русский

Кольцо целых ℚ естественно эквивалентно ℤ; они изоморфны как кольца.

LaTeX

$$$\\mathcal{O}_{\\mathbb{Q}} \\cong \\mathbb{Z}.$$$

Lean4

/-- The ring of integers of `ℚ` as a number field is just `ℤ`. -/
noncomputable def ringOfIntegersEquiv : 𝓞 ℚ ≃+* ℤ :=
  RingOfIntegers.equiv ℤ

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

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

Разделы

Аффилиация

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