ascPochhammer_succ_comp_X_add_one

English

For any S with no zero divisors, ascPochhammer S n is a monic polynomial.

Русский

Для любого S без делителей нуля ascPochhammer S n является моническим многочленом.

LaTeX

$$$(ascPochhammer S n).Monic$$$

Lean4

theorem ascPochhammer_succ_comp_X_add_one (n : ℕ) :
    (ascPochhammer S (n + 1)).comp (X + 1) = ascPochhammer S (n + 1) + (n + 1) • (ascPochhammer S n).comp (X + 1) :=
  by
  suffices (ascPochhammer ℕ (n + 1)).comp (X + 1) = ascPochhammer ℕ (n + 1) + (n + 1) * (ascPochhammer ℕ n).comp (X + 1)
    by simpa [map_comp] using congr_arg (Polynomial.map (Nat.castRingHom S)) this
  nth_rw 2 [ascPochhammer_succ_left]
  rw [← add_mul, ascPochhammer_succ_right ℕ n, mul_comp, mul_comm, add_comp, X_comp, natCast_comp, add_comm, ←
    add_assoc]
  ring

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