integralClosure

Mathlib.RingTheory.Valuation.Integral

URI: https://scilib.ai/kg/mathlib#Valuation.Integers.integralClosure

← MathLib Explorer

English

The valuation integer subring is integrally closed.

Русский

Подкольцо целочисленных значений является целиком замкнутым.

LaTeX

$$IsIntegrallyClosed O$$

Lean4

protected theorem integralClosure : integralClosure O R = ⊥ :=
  bot_unique fun _ hr =>
    let ⟨x, hx⟩ := hv.3 (hv.mem_of_integral hr)
    Algebra.mem_bot.2 ⟨x, hx⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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