natDegree_lt_natDegree_iff — Mathlib

English

For p ≠ 0, natDegree p < natDegree q iff degree p < degree q.

Русский

Для p ≠ 0: natDegree p < natDegree q эквивалентно degree p < degree q.

LaTeX

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

Lean4

theorem natDegree_lt_natDegree_iff (hp : p ≠ 0) : natDegree p < natDegree q ↔ degree p < degree q :=
  ⟨degree_lt_degree, fun h ↦ by
    have hq : q ≠ 0 := ne_zero_of_degree_gt h
    rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at h⟩

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