liftHom_map — Mathlib

English

For any z ∈ R[X], the liftHom evaluated at h.map z equals aeval x z, i.e., h.liftHom x hx' (h.map z) = aeval x z.

Русский

Для любого z ∈ R[X] отображение h.liftHom над z удовлетворяет h.liftHom x hx' (h.map z) = aeval x z.

LaTeX

$$$ h.liftHom x hx' (h.map z) = \operatorname{aeval}_x(z) $$$

Lean4

@[simp]
theorem liftHom_map (z : R[X]) : h.liftHom x hx' (h.map z) = aeval x z := by
  rw [← lift_algebraMap_apply, lift_map, aeval_def]

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