descPochhammer_eq_ascPochhammer — Mathlib

English

For all n, the polynomial descPochhammer R n is monic (leading coefficient 1) provided R is a nontrivial ring with no zero divisors.

Русский

Для всех n полином descPochhammer R n является моноичным при условии, что R ненулево и без нулевых делителей.

LaTeX

$$(descPochhammer R n).Monic$$

Lean4

theorem descPochhammer_eq_ascPochhammer (n : ℕ) : descPochhammer ℤ n = (ascPochhammer ℤ n).comp ((X : ℤ[X]) - n + 1) :=
  by
  induction n with
  | zero => rw [descPochhammer_zero, ascPochhammer_zero, one_comp]
  | succ n ih =>
    rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right, ascPochhammer_succ_left, ih, X_mul,
      mul_X_comp, comp_assoc, add_comp, X_comp, one_comp]

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