instIsIntegrallyClosed

Mathlib.NumberTheory.NumberField.Basic

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

English

𝓞_K is integrally closed in K.

Русский

𝓞_K интегрально замкнуто в K.

LaTeX

$$$𝓞_K \\text{ is integrally closed in } K$$$

Lean4

instance [NumberField K] : IsIntegrallyClosed (𝓞 K) :=
  integralClosure.isIntegrallyClosedOfFiniteExtension ℚ

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

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

Разделы

Аффилиация

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