spectralValue_X_pow — Mathlib

English

The spectral value of X^n is 0 for any natural n.

Русский

Спектральное значение X^n равно 0 для любого натурального n.

LaTeX

$$$$\operatorname{spectralValue}(X^n) = 0.$$$$

Lean4

/-- The polynomial `X ^ n` has spectral value `0`. -/
theorem spectralValue_X_pow (n : ℕ) : spectralValue (X ^ n : R[X]) = 0 :=
  by
  rw [spectralValue]
  unfold spectralValueTerms
  simp_rw [coeff_X_pow n, natDegree_X_pow]
  convert ciSup_const using 2
  · ext m
    by_cases hmn : m < n
    · rw [if_pos hmn, rpow_eq_zero_iff_of_nonneg (norm_nonneg _), if_neg (_root_.ne_of_lt hmn), norm_zero, one_div,
        ne_eq, inv_eq_zero, ← cast_sub (le_of_lt hmn), cast_eq_zero, Nat.sub_eq_zero_iff_le]
      exact ⟨Eq.refl _, not_le_of_gt hmn⟩
    · rw [if_neg hmn]
  · infer_instance

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