natTrailingDegree_le_trailingDegree

English

If trailingDegree(p) = trailingDegree(q), then natTrailingDegree(p) = natTrailingDegree(q).

Русский

Если хвостовые степени p и q равны, то natTrailingDegree(p) = natTrailingDegree(q).

LaTeX

$$$\operatorname{trailingDegree}(p) = \operatorname{trailingDegree}(q) \Rightarrow \operatorname{natTrailingDegree}(p) = \operatorname{natTrailingDegree}(q)$$$

Lean4

@[simp]
theorem natTrailingDegree_le_trailingDegree : ↑(natTrailingDegree p) ≤ trailingDegree p :=
  ENat.coe_toNat_le_self _

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