monic_ascPochhammer — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem monic_ascPochhammer (n : ℕ) [Nontrivial S] [NoZeroDivisors S] : Monic <| ascPochhammer S n := by
  induction n with
  | zero => simp
  | succ n hn =>
    have : leadingCoeff (X + 1 : S[X]) = 1 := leadingCoeff_X_add_C 1
    rw [ascPochhammer_succ_left, Monic.def, leadingCoeff_mul,
      leadingCoeff_comp (ne_zero_of_eq_one <| natDegree_X_add_C 1 : natDegree (X + 1) ≠ 0), hn, monic_X, one_mul,
      one_mul, this, one_pow]

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