ofFn_natDegree_lt — Mathlib

English

For n ≥ 1 and v ∈ Fin n → R, the natural degree of ofFn n v is less than n.

Русский

Для n ≥ 1 и v ∈ Fin n → R, natDegree(ofFn n v) < n.

LaTeX

$$$(\operatorname{natDegree}((\operatorname{ofFn}(n)\, v))) < n.$$$

Lean4

/-- `ofFn n v` has `natDegree` smaller than `n`. -/
theorem ofFn_natDegree_lt {n : ℕ} (h : 1 ≤ n) (v : Fin n → R) : (ofFn n v).natDegree < n :=
  by
  rw [Nat.lt_iff_le_pred h, natDegree_le_iff_coeff_eq_zero]
  exact fun _ h ↦ ofFn_coeff_eq_zero_of_ge _ <| Nat.le_of_pred_lt h

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