sort_roots_charpoly_eq_eigenvalues₀

English

The sorted real roots of the characteristic polynomial match the sorted eigenvalues₀ when ordered by the natural order.

Русский

Отсортированные по невозрастанию корни характеристического многочлена совпадают с отсортированными eigenvalues₀.

LaTeX

$$$(A.charpoly.roots.map \mathbb{R}).sort(\ge) = \text{List.ofFn}(h_A.eigenvalues_0)$$$

Lean4

theorem sort_roots_charpoly_eq_eigenvalues₀ :
    (A.charpoly.roots.map RCLike.re).sort (· ≥ ·) = List.ofFn hA.eigenvalues₀ :=
  by
  simp_rw [hA.roots_charpoly_eq_eigenvalues₀, Fin.univ_val_map, Multiset.map_coe, List.map_ofFn, Function.comp_def,
    RCLike.ofReal_re, Multiset.coe_sort]
  rw [List.mergeSort_of_sorted]
  simpa [List.Sorted] using (eigenvalues₀_antitone hA).ofFn_sorted

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