ascPochhammer_eval₂ — Mathlib

English

For any ring hom f:S→+*T, the two-variable evaluation relation holds: (ascPochhammer T n).eval t = (ascPochhammer S n).eval₂ f t.

Русский

Для любого гомоморфа f: S→+*T верно равенство: (ascPochhammer T n).eval t = (ascPochhammer S n).eval₂ f t.

LaTeX

$$$ (ascPochhammer T\\, n).\\mathrm{eval}\\ t = (ascPochhammer S\\, n).\\mathrm{eval_2}\\ f\\ t $$$

Lean4

theorem ascPochhammer_eval₂ (f : S →+* T) (n : ℕ) (t : T) :
    (ascPochhammer T n).eval t = (ascPochhammer S n).eval₂ f t :=
  by
  rw [← ascPochhammer_map f]
  exact eval_map f t

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