ascPochhammer_eval_cast — Mathlib

English

For semiring S, and natural n, k, the evaluation under nat casting commutes with ascPochhammer: the cast of the Nat evaluation equals the S-evaluation.

Русский

Для полугруппы S и натуральных n, k исполнение через приведение к S-компонентам совпадает с оценкой, полученной в S.

LaTeX

$$$\\mathrm{Nat.cast}\\big(((ascPochhammer\\,\\mathbb{N}\\, n).\\mathrm{eval}\\ k)\\big) = ((ascPochhammer\\, S\\, n).\\mathrm{eval}\\ k)\\,\\mathrm{cast}$$$

Lean4

@[simp, norm_cast]
theorem ascPochhammer_eval_cast (n k : ℕ) : (((ascPochhammer ℕ n).eval k : ℕ) : S) = ((ascPochhammer S n).eval k : S) :=
  by rw [← ascPochhammer_map (algebraMap ℕ S), eval_map, ← eq_natCast (algebraMap ℕ S), eval₂_at_natCast, Nat.cast_id]

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