English
For any ring R with the given structure, smeval (ascPochhammer ℤ n) r equals smeval (ascPochhammer ℕ n) r for all n ∈ ℕ. This shows consistency between integer and natural parameterizations in smeval.
Русский
Для любого кольца R соблюдается: smeval(ascPochhammer ℤ n) r = smeval(ascPochhammer ℕ n) r для всех n ∈ ℕ.
LaTeX
$$$ \forall R\ [NonAssocRing\ R]\ [Pow\ R\ \mathbb{N}]\ [NatPowAssoc\ R]\ (r:\,R)\,\forall n:\,\mathbb{N},\ \mathrm{smeval}(\ascPochhammer\ \mathbb{Z}\ n)\,r = \mathrm{smeval}(\ascPochhammer\ \mathbb{N}\ n)\,r$$$
Lean4
theorem smeval_ascPochhammer_int_ofNat {R} [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] (r : R) :
∀ n : ℕ, smeval (ascPochhammer ℤ n) r = smeval (ascPochhammer ℕ n) r
| 0 => by simp only [ascPochhammer_zero, smeval_one]
| n + 1 => by
simp only [ascPochhammer_succ_right, smeval_mul]
rw [smeval_ascPochhammer_int_ofNat r n]
simp only [smeval_add, smeval_X, ← C_eq_natCast, smeval_C, natCast_zsmul, nsmul_eq_mul, Nat.cast_id]
