coe_liftHom — Mathlib

English

The underlying ring hom of liftHom f a hfx is exactly lift (algebraMap R S) a hfx.

Русский

Основной гомоморфизм-подпись liftHom совпадает с аналогичным стандартным подъемом.

LaTeX

$$$(liftHom f a hfx : AdjoinRoot f \\to_{R} S) = lift (\\mathrm{algebraMap}\\ R S) a hfx$$$

Lean4

@[simp]
theorem coe_liftHom (x : S) (hfx : aeval x f = 0) :
    (liftHom f x hfx : AdjoinRoot f →+* S) = lift (algebraMap R S) x hfx :=
  rfl

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