withBotSucc_degree_eq_natDegree_add_one

English

For any nonzero polynomial p, the successor of its degree equals natDegree(p) + 1.

Русский

Для ненулевого многочлена p переход к следующей степени равен natDegree(p) + 1.

LaTeX

$$$ (\deg p).\text{succ} = \operatorname{natDegree}(p) + 1 \quad\text{при } p \neq 0 $$

Lean4

theorem withBotSucc_degree_eq_natDegree_add_one (h : p ≠ 0) : p.degree.succ = p.natDegree + 1 :=
  by
  rw [degree_eq_natDegree h]
  exact WithBot.succ_coe p.natDegree

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