liftHom_algEquiv — Mathlib

English

With liftHom, the same compatibility holds when restricting to a different target algebra U; i.e., h'.liftHom x hx (h.algEquiv h' z) = h.liftHom x hx z.

Русский

Для liftHom выполняется та же совместимость при смене целевого кольца U.

LaTeX

$$h'.liftHom x hx (h.algEquiv h' z) = h.liftHom x hx z$$

Lean4

@[simp]
theorem liftHom_algEquiv [Algebra R U] (x : U) (hx z) : h'.liftHom x hx (h.algEquiv h' z) = h.liftHom x hx z :=
  h.lift_algEquiv h' _ _ hx _

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