AlgebraIsIntegral

Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

URI: https://scilib.ai/kg/mathlib#integralClosure.AlgebraIsIntegral

English

Every element of the integral closure is integral over R.

Русский

Каждый элемент интегрального замыкания интегрален над R.

LaTeX

$$$IsIntegral R x$ for $x \in integralClosure R A$$$

Lean4

instance AlgebraIsIntegral : Algebra.IsIntegral R (integralClosure R A) :=
  ⟨integralClosure.isIntegral⟩

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

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

Разделы

Аффилиация

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