trailingDegree_le_trailingDegree — Mathlib

English

If coeff q(natTrailingDegree(p)) ≠ 0, then trailingDegree q ≤ trailingDegree p.

Русский

Если коэффициент q на позиции natTrailingDegree(p) не равен 0, то trailingDegree(q) ≤ trailingDegree(p).

LaTeX

$$$\operatorname{coeff}(q, \operatorname{natTrailingDegree}(p)) \neq 0 \Rightarrow \operatorname{trailingDegree}(q) \le \operatorname{trailingDegree}(p)$$$

Lean4

@[simp]
theorem trailingDegree_le_trailingDegree (h : coeff q (natTrailingDegree p) ≠ 0) :
    trailingDegree q ≤ trailingDegree p :=
  (trailingDegree_le_of_ne_zero h).trans natTrailingDegree_le_trailingDegree

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