degree_le_degree — Mathlib

English

If the coefficient of q at natDegree p is nonzero, then degree p ≤ degree q.

Русский

Если коэффициент q при natDegree(p) не равен нулю, то deg p ≤ deg q.

LaTeX

$$$ (q.coeff(p.natDegree) \neq 0) \Rightarrow \deg(p) \le \deg(q) $$$

Lean4

theorem degree_le_degree (h : coeff q (natDegree p) ≠ 0) : degree p ≤ degree q :=
  by
  by_cases hp : p = 0
  · rw [hp, degree_zero]
    exact bot_le
  · rw [degree_eq_natDegree hp]
    exact le_degree_of_ne_zero h

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