natDegree_eq_support_max' — Mathlib

English

If p ≠ 0, then natDegree(p) equals the maximum element of the support of p.

Русский

Если p ≠ 0, то natDegree(p) равно максимальному элементу из supp(p).

LaTeX

$$$p \neq 0 \Rightarrow \operatorname{natDegree}(p) = \operatorname{supp}(p).max'(\operatorname{nonempty_support_iff.mpr}(p \neq 0)).$$$

Lean4

theorem natDegree_eq_support_max' (h : p ≠ 0) : p.natDegree = p.support.max' (nonempty_support_iff.mpr h) :=
  (le_max' _ _ <| natDegree_mem_support_of_nonzero h).antisymm <| max'_le _ _ _ le_natDegree_of_mem_supp

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