English
The smeval of ascPochhammer under cast invariance equals the smeval at Nat-nat cast. In any semiring R and suitable S with a module structure, the cast does not affect the smeval of ascPochhammer.
Русский
Переход по приведениям (cast) не изменяет smeval для ascPochhammer; тождество сохраняется в рамках допустимых колец и модулей.
LaTeX
$$$\text{ascPochhammer}(R,n)\text{.smeval}_{x} = \text{ascPochhammer}(\mathbb{N},n)\text{.smeval}_{x}$$$
Lean4
@[simp]
theorem ascPochhammer_smeval_cast (R : Type*) [Semiring R] {S : Type*} [NonAssocSemiring S] [Pow S ℕ] [Module R S]
[IsScalarTower R S S] [NatPowAssoc S] (x : S) (n : ℕ) :
(ascPochhammer R n).smeval x = (ascPochhammer ℕ n).smeval x := by
induction n with
| zero => simp only [ascPochhammer_zero, smeval_one, one_smul]
| succ n hn =>
simp only [ascPochhammer_succ_right, mul_add, smeval_add, smeval_mul_X, ← Nat.cast_comm]
simp only [← C_eq_natCast, smeval_C_mul, hn, Nat.cast_smul_eq_nsmul R n]
simp only [nsmul_eq_mul, Nat.cast_id]
