lift_self

Mathlib.RingTheory.IsAdjoinRoot

URI: https://scilib.ai/kg/mathlib#IsAdjoinRoot.lift_self

English

The lift equals the identity map: the lifted hom equals id_S.

Русский

Поднятое отображение равно тождественному отображению: lift равно id_S.

LaTeX

$$$ h.lift(\\text{algebraMap } R S) h.root h.aeval\\_root\\_self = \\text{RingHom}.id S $$$

Lean4

theorem lift_self : h.lift (algebraMap R S) h.root h.aeval_root_self = RingHom.id S :=
  RingHom.ext h.lift_self_apply

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

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

Разделы

Аффилиация

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