coe_lt_degree — Mathlib

English

For any polynomial p and natural n, (n, as a WithBot ℕ) less than deg p is equivalent to n < natDegree p, with the case p = 0 handled by simp.

Русский

Для любого полинома p и натурального n: (n в WithBot ℕ) меньше deg p эквивалентно n < natDegree p; случай p = 0 обрабатывается автоматически.

LaTeX

$$$ (n : \WithBot \mathbb{N}) < \deg p \;\iff\; n < \operatorname{natDegree}(p) $$$

Lean4

@[simp]
theorem coe_lt_degree {p : R[X]} {n : ℕ} : (n : WithBot ℕ) < degree p ↔ n < natDegree p :=
  by
  by_cases h : p = 0
  · simp [h]
  simp [degree_eq_natDegree h, Nat.cast_lt]

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