lift_algebraMap_apply — Mathlib

English

Applying the lifted map to an element z ∈ S agrees with applying the lifted algebra map to z, i.e., h.lift (algebraMap R T) x hx' z = h.liftHom x hx' z.

Русский

Применение лифта к элементу z ∈ S согласуется с применением поднимаемой алгебраической карты к z: h.lift (algebraMap R T) x hx' z = h.liftHom x hx' z.

LaTeX

$$$ h.lift (algebraMap R T) x hx' z = h.liftHom x hx' z $$$

Lean4

theorem lift_algebraMap_apply (z : S) : h.lift (algebraMap R T) x hx' z = h.liftHom x hx' z :=
  rfl

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