natDegree_lt_iff_degree_lt — Mathlib

English

Let p ≠ 0. Then p.natDegree < n iff p.degree < n (with the appropriate cast from n to the degree type).

Русский

Пусть p ≠ 0. Тогда p.natDegree < n эквивалентно p.degree < n (с привидением типа n к соответствующему боксу степени).

LaTeX

$$p \\neq 0 \\Rightarrow p.natDegree < n \\iff p.degree < n.cast$$

Lean4

theorem natDegree_lt_iff_degree_lt (hp : p ≠ 0) : p.natDegree < n ↔ p.degree < ↑n :=
  WithBot.unbotD_lt_iff (absurd · (degree_eq_bot.not.mpr hp))

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