natDegree_lt_natDegree — Mathlib

English

Let p ∈ R[X] and q ∈ S[X] with p ≠ 0 and deg p < deg q. Then natDegree(p) < natDegree(q).

Русский

Пусть p ∈ R[X], q ∈ S[X], p ≠ 0 и deg p < deg q. Тогда natDegree(p) < natDegree(q).

LaTeX

$$$ p \in R[X], q \in S[X], p \neq 0 \land p.degree < q.degree \Rightarrow p.natDegree < q.natDegree $$$

Lean4

theorem natDegree_lt_natDegree {q : S[X]} (hp : p ≠ 0) (hpq : p.degree < q.degree) : p.natDegree < q.natDegree :=
  by
  by_cases hq : q = 0
  · exact (not_lt_bot <| hq ▸ hpq).elim
  rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at hpq

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