descPochhammer_eval_cast — Mathlib

English

The evaluation of descPochhammer at integers commutes with integer-to-ring casts: casting the value from Z to R matches the evaluation in R.

Русский

Оценка descPochhammer при целых числах совместима с привидением целого к кольцу: перевод значения из Z в R совпадает с оценкой в R.

LaTeX

$$$\big( (\descPochhammer\;\mathbb{Z}\; n).eval\; k \big) \;^{\;\text{cast}} = (\descPochhammer\; R\; n).eval\; k$$$

Lean4

@[simp, norm_cast]
theorem descPochhammer_eval_cast (n : ℕ) (k : ℤ) :
    (((descPochhammer ℤ n).eval k : ℤ) : R) = ((descPochhammer R n).eval k : R) :=
  by
  rw [← descPochhammer_map (algebraMap ℤ R), eval_map, ← eq_intCast (algebraMap ℤ R)]
  simp only [algebraMap_int_eq, eq_intCast, eval₂_at_intCast, Int.cast_id]

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