degree_eq_natDegree — Mathlib

English

If p ≠ 0, then degree(p) = (natDegree(p) : WithBot ℕ).

Русский

Если p ≠ 0, то degree(p) = (natDegree(p) : WithBot ℕ).

LaTeX

$$$\deg(p) = (\operatorname{natDegree}(p) : \mathrm{WithBot} \, \mathbb{N})$$$

Lean4

theorem degree_eq_natDegree (hp : p ≠ 0) : degree p = (natDegree p : WithBot ℕ) :=
  by
  let ⟨n, hn⟩ := not_forall.1 (mt Option.eq_none_iff_forall_not_mem.2 (mt degree_eq_bot.1 hp))
  have hn : degree p = some n := Classical.not_not.1 hn
  rw [natDegree, hn]; rfl

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