isIntegralElem_one

Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

URI: https://scilib.ai/kg/mathlib#RingHom.isIntegralElem_one

English

The unity element 1 is integral over the base ring in any algebra extension.

Русский

Единица 1 интегральна над базовым кольцом в любой алгебральной расширении.

LaTeX

$$$1\\in B$ integral over R$$

Lean4

theorem isIntegralElem_one : f.IsIntegralElem 1 :=
  f.map_one ▸ f.isIntegralElem_map

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

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

Разделы

Аффилиация

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