spectralValueTerms_of_natDegree_le

English

If p is a polynomial with degree not smaller than n, spectralValueTerms p n is zero whenever n ≥ natDegree(p).

Русский

Если n ≥ natDegree(p), то spectralValueTerms(p)(n) = 0.

LaTeX

$$$$\operatorname{spectralValueTerms}(p)(n)=0\quad\text{если } p.natDegree\le n,$$$$

Lean4

theorem spectralValueTerms_of_natDegree_le (p : R[X]) {n : ℕ} (hn : p.natDegree ≤ n) : spectralValueTerms p n = 0 := by
  simp only [spectralValueTerms, if_neg (not_lt.mpr hn)]

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