integralClosure_le_algebraicClosure

Mathlib.RingTheory.Algebraic.Integral

URI: https://scilib.ai/kg/mathlib#integralClosure_le_algebraicClosure

English

In the setting, every element integral over R lies inside the algebraicClosure R S.

Русский

Каждый элемент, интеграционный над R, лежит внутри algebraicClosure R S.

LaTeX

$$$\\text{integralClosure}_R S \\le \\text{algebraicClosure}_R S$$$

Lean4

theorem integralClosure_le_algebraicClosure [IsDomain R] : integralClosure R S ≤ Subalgebra.algebraicClosure R S :=
  fun _ ↦ IsIntegral.isAlgebraic

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

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

Разделы

Аффилиация

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