coe_liftHom — Mathlib

English

The coercion of liftHom equals lift with algebraMap, i.e., the concrete representation of h.liftHom coincides with h.lift (algebraMap R T) x hx'.

Русский

Приведение к LiftHom совпадает с Lift через algebraMap, т.е. точная запись h.liftHom совпадает с h.lift (algebraMap R T) x hx'.

LaTeX

$$$ (h.liftHom x hx' : S \to_{R} T) = h.lift (algebraMap R T) x hx' $$$

Lean4

@[simp]
theorem coe_liftHom : (h.liftHom x hx' : S →+* T) = h.lift (algebraMap R T) x hx' :=
  rfl

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