liftHom_root

Mathlib.RingTheory.AdjoinRoot

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

English

The liftHom_mk formula: liftHom f a hfx (mk f g) = aeval a g; i.e., map respects polynomial evaluation on mk.

Русский

Формула liftHom_mk: liftHom f a hfx (mk f g) = aeval a g.

LaTeX

$$$liftHom\\ f\\ a\\ hfx\\ (mk\\ f\\ g) = aeval\\ a\\ g$$$

Lean4

@[simp]
theorem liftHom_root : liftHom f a hfx (root f) = a :=
  lift_root hfx

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

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

Разделы

Аффилиация

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