natTrailingDegree_le_natTrailingDegree

English

If q ≠ 0 and p.trailingDegree ≤ q.trailingDegree then p.natTrailingDegree ≤ q.natTrailingDegree.

Русский

Если q ≠ 0 и p.trailingDegree ≤ q.trailingDegree, то p.natTrailingDegree ≤ q.natTrailingDegree.

LaTeX

$$$q \neq 0 \Rightarrow p.trailingDegree \le q.trailingDegree \Rightarrow p.natTrailingDegree \le q.natTrailingDegree$$$

Lean4

theorem natTrailingDegree_le_natTrailingDegree (hq : q ≠ 0) (hpq : p.trailingDegree ≤ q.trailingDegree) :
    p.natTrailingDegree ≤ q.natTrailingDegree :=
  ENat.toNat_le_toNat hpq <| by simpa

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