ascPochhammer_map — Mathlib

English

For any ring homomorphism f:S→+*T, the map commutes with ascPochhammer: map f (ascPochhammer S n) = ascPochhammer T n.

Русский

Любое отображение полиномов сохраняетascPochhammer: map f (ascPochhammer S n) = ascPochhammer T n.

LaTeX

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

Lean4

@[simp]
theorem ascPochhammer_map (f : S →+* T) (n : ℕ) : (ascPochhammer S n).map f = ascPochhammer T n := by
  induction n with
  | zero => simp
  | succ n ih => simp [ih, ascPochhammer_succ_left, map_comp]

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