degree_shiftedLegendre — Mathlib

English

The degree of shiftedLegendre n is n.

Русский

Степень shiftedLegendre n равна n.

LaTeX

$$$\\operatorname{degree}(\\mathrm{shiftedLegendre}(n)) = n$$$

Lean4

/-- The degree of `shiftedLegendre n` is `n`. -/
@[simp]
theorem degree_shiftedLegendre (n : ℕ) : (shiftedLegendre n).degree = n :=
  by
  refine le_antisymm ?_ (le_degree_of_ne_zero ?_)
  · rw [degree_le_iff_coeff_zero]
    intro k h
    norm_cast at h
    simp [coeff_shiftedLegendre, choose_eq_zero_of_lt h]
  · simp [coeff_shiftedLegendre, (choose_pos (show n ≤ n + n by simp)).ne']

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