descPochhammer_natDegree — Mathlib

English

The natural degree of the descending Pochhammer polynomial is n: natDegree(descPochhammer R n) = n.

Русский

Натуральная степень(descPochhammer R n) равна n: natDegree(descPochhammer R n) = n.

LaTeX

$$$(\operatorname{natDegree}(\operatorname{descPochhammer}_R(n))) = n$$$

Lean4

@[simp]
theorem descPochhammer_natDegree (n : ℕ) [NoZeroDivisors R] [Nontrivial R] : (descPochhammer R n).natDegree = n := by
  induction n with
  | zero => simp
  | succ n hn =>
    have : natDegree (X - (n : R[X])) = 1 := natDegree_X_sub_C (n : R)
    rw [descPochhammer_succ_right, natDegree_mul _ (ne_zero_of_natDegree_gt <| this.symm ▸ Nat.zero_lt_one), hn, this]
    cases n
    · simp
    · refine ne_zero_of_natDegree_gt <| hn.symm ▸ Nat.add_one_pos _

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