English
The eigenvalues of the diagonal linear operator with respect to standard basis are exactly the diagonal entries.
Русский
Собственные значения диагонального линейного отображения по отношению к стандартному базису равны самим диагональным элементам.
LaTeX
$$$\\text{HasEigenvalue}\\_{{diagonal}} \\leftrightarrow \\exists i, d_i = μ$$$
Lean4
@[simp]
theorem maxGenEigenspace_toLin_diagonal_eq_eigenspace [IsDomain R] :
maxGenEigenspace ((diagonal d).toLin b b) μ = eigenspace ((diagonal d).toLin b b) μ :=
by
refine le_antisymm (fun x hx ↦ ?_) eigenspace_le_maxGenEigenspace
obtain ⟨k, hk⟩ := (mem_maxGenEigenspace _ _ _).mp hx
replace hk (j : n) : b.repr x j = 0 ∨ d j = μ ∧ k ≠ 0 :=
by
have aux : (diagonal d).toLin b b - μ • 1 = (diagonal (d - μ • 1)).toLin b b := by rw [Pi.sub_def, ← diagonal_sub];
simp [one_eq_id]
rw [aux, ← toLin_pow, diagonal_pow, toLin_apply_eq_zero_iff] at hk
simpa [mulVec_eq_sum, diagonal_apply, sub_eq_zero] using hk j
have aux (j : n) : (b.repr x j * d j) • b j = μ • (b.repr x j • b j) :=
by
rcases hk j with hj | hj
· simp [hj]
· rw [← hj.1, mul_comm, MulAction.mul_smul]
simp [toLin_apply, mulVec_eq_sum, diagonal_apply, aux, ← Finset.smul_sum]
