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