liftHom_root

Mathlib.RingTheory.IsAdjoinRoot

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

English

The root is preserved by liftHom: h.liftHom x hx' h.root = x.

Русский

Корень сохраняется под LiftHom: h.liftHom x hx' h.root = x.

LaTeX

$$$ h.liftHom x hx' h.root = x $$$

Lean4

@[simp]
theorem liftHom_root : h.liftHom x hx' h.root = x := by rw [← lift_algebraMap_apply, lift_root]

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

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

Разделы

Аффилиация

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