supDegree_eq_natDegree — Mathlib

English

For any polynomial p, p.toFinsupp.supDegree id = p.natDegree.

Русский

Для любого полинома p выражение p.toFinsupp.supDegree id равно p.natDegree.

LaTeX

$$p.toFinsupp.supDegree id = p.natDegree$$

Lean4

theorem supDegree_eq_natDegree (p : R[X]) : p.toFinsupp.supDegree id = p.natDegree :=
  by
  obtain rfl | h := eq_or_ne p 0
  · simp
  apply WithBot.coe_injective
  rw [← AddMonoidAlgebra.supDegree_withBot_some_comp, Function.comp_id, supDegree_eq_degree, degree_eq_natDegree h,
    Nat.cast_withBot]
  rwa [support_toFinsupp, nonempty_iff_ne_empty, Ne, support_eq_empty]

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