isIntegral_one

Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

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

English

The element 1 is integral over the base ring.

Русский

Элемент 1 интегрален над базовым кольцом.

LaTeX

$$$\\text{IsIntegral}_R(1)$$$

Lean4

theorem isIntegral_one [Algebra R B] : IsIntegral R (1 : B) :=
  (algebraMap R B).isIntegralElem_one

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

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

Разделы

Аффилиация

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