instIsFractionRing

Mathlib.NumberTheory.NumberField.Basic

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

English

The ring of integers 𝓞_K is a subring of K whose field of fractions is K.

Русский

Кольцо целых 𝓞_K является подкольцом K, у которого поле дробей равно K.

LaTeX

$$$\\operatorname{Frac}(\\mathcal{O}_K) = K$$$

Lean4

instance [NumberField K] : IsFractionRing (𝓞 K) K :=
  integralClosure.isFractionRing_of_finite_extension ℚ _

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

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

Разделы

Аффилиация

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