degreeLT_succ_eq_degreeLE — Mathlib

English

The degreeLT of n+1 equals degreeLE of n; i.e., polynomials of degree < n+1 are exactly those of degree ≤ n.

Русский

Степень degreeLT(n+1) равна degreeLE(n); то есть многочлены степени < n+1 эквивалентны тем, которые имеют deg ≤ n.

LaTeX

$$$\operatorname{degreeLT}_R(n+1) = \operatorname{degreeLE}_R(n).$$$

Lean4

theorem degreeLT_succ_eq_degreeLE {n : ℕ} : degreeLT R (n + 1) = degreeLE R n :=
  by
  ext x
  by_cases x_zero : x = 0
  · simp_rw [x_zero, Submodule.zero_mem]
  ·
    rw [mem_degreeLT, mem_degreeLE, ← natDegree_lt_iff_degree_lt (by rwa [ne_eq]), ← natDegree_le_iff_degree_le,
      Nat.lt_succ]

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