degree_lt_degree — Mathlib

English

If natDegree p < natDegree q then degree p < degree q.

Русский

Если natDegree p < natDegree q, то degree p < degree q.

LaTeX

$$$ p, q \in R[X], p \neq 0 \Rightarrow [\operatorname{natDegree}(p) < \operatorname{natDegree}(q) \Rightarrow \deg(p) < \deg(q)] $$$

Lean4

theorem degree_lt_degree (h : natDegree p < natDegree q) : degree p < degree q :=
  by
  by_cases hp : p = 0
  · simp only [hp, degree_zero]
    rw [bot_lt_iff_ne_bot]
    intro hq
    simp [hp, degree_eq_bot.mp hq] at h
  · rwa [degree_eq_natDegree hp, degree_eq_natDegree <| ne_zero_of_natDegree_gt h, Nat.cast_lt]

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