instIsIntegralClosureInt

Mathlib.NumberTheory.NumberField.Basic

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

English

𝓞_K is the integral closure of ℤ in K.

Русский

𝓞_K является интегральным замыканием ℤ в K.

LaTeX

$$$\\mathcal{O}_K$ is the integral closure of $\\mathbb{Z}$ in $K$.$$

Lean4

instance : IsIntegralClosure (𝓞 K) ℤ K :=
  integralClosure.isIntegralClosure _ _

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

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

Разделы

Аффилиация

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