liftHom_of

Mathlib.RingTheory.AdjoinRoot

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

English

If ϕ is an algebra hom AdjoinRoot f → S, then aeval (ϕ(root f)) f = 0.

Русский

Если ϕ — алгебра-гомоморф AdjoinRoot f → S, то aeval(ϕ(root f)) f = 0.

LaTeX

$$$\\mathrm{aeval}(\\ϕ(\\mathrm{root} f)) f = 0$$$

Lean4

@[simp]
theorem liftHom_of {x : R} : liftHom f a hfx (of f x) = algebraMap _ _ x :=
  lift_of hfx

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

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

Разделы

Аффилиация

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