ascPochhammer_mul — Mathlib

English

Same as 182918: the map commutes with ascPochhammer under ring homomorphism.

Русский

То же самое, что и в 182918: отображение сохраняет ascPochhammer под кольцевым гомоморфизмом.

LaTeX

$$$\\mathrm{map}\\ f\\ (ascPochhammer\\ S\\ n) = ascPochhammer\\ T\\ n$$$

Lean4

theorem ascPochhammer_mul (n m : ℕ) :
    ascPochhammer S n * (ascPochhammer S m).comp (X + (n : S[X])) = ascPochhammer S (n + m) := by
  induction m with
  | zero => simp
  | succ m ih =>
    rw [ascPochhammer_succ_right, Polynomial.mul_X_add_natCast_comp, ← mul_assoc, ih, ← add_assoc,
      ascPochhammer_succ_right, Nat.cast_add, add_assoc]

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