ascPochhammer_natDegree — Mathlib

English

If S has no zero divisors and is nontrivial, then (ascPochhammer S n).natDegree = n.

Русский

Если S не имеет нулевых делителей и ненулево, то nattDegree ascPochhammer S n равен n.

LaTeX

$$$(ascPochhammer S n).natDegree = n$$$

Lean4

@[simp]
theorem ascPochhammer_natDegree (n : ℕ) [NoZeroDivisors S] [Nontrivial S] : (ascPochhammer S n).natDegree = n := by
  induction n with
  | zero => simp
  | succ n hn =>
    have : natDegree (X + (n : S[X])) = 1 := natDegree_X_add_C (n : S)
    rw [ascPochhammer_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 _

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