Revision #1177 → #1817 · back to history
modifiedEquivalence of matrix and linear-transformation definitions7ce8580ec1d3
| Field | From #1177 | To #1817 |
|---|
| note | `LinearMap.spectrum_toMatrix` and `Matrix.spectrum_toLin` show the spectra agree under `toMatrix`/`toLin`. | `LinearMap.spectrum_toMatrix` shows the spectra agree under `toMatrix`/`toLin`. |
modifiedCharacteristic equation via determinant1aa582c83f5d
| Field | From #1177 | To #1817 |
|---|
| note | Eigenvalues are exactly the roots of the characteristic polynomial; equivalently `det(λI − A) = 0` via `eval_charpoly`. | Eigenvalues are exactly the roots of the characteristic polynomial, equivalently `det(λI − A) = 0`. |
modifiedFactoring the characteristic polynomial2258deabe732
| Field | From #1177 | To #1817 |
|---|
| note | `charpoly_natDegree` gives degree `n`; `Polynomial.card_roots_le_degree` bounds the roots. | `charpoly_natDegree` gives degree `n`; combined with degree bounds on root counts, this matches the at-most-n claim. |
modifiedComplex conjugate eigenvalue pairsf140fe9cec43
| Field | From #1177 | To #1817 |
|---|
| mathlib.decl | Polynomial.isRoot_conj_of_isRoot | Polynomial.aeval_conj |
| mathlib.module | Mathlib.Analysis.Complex.Polynomial.Basic | Mathlib.Analysis.RCLike.Lemmas |
| note | General fact about conjugate roots of real polynomials exists; not specialized to eigenvalues. | `Polynomial.aeval_conj` shows `aeval (conj z) p = conj (aeval z p)` for real polynomials, implying conjugate pairs of non-real roots; not specialized to eigenvalues. |
modifiedAlgebraic multiplicityfb7068b487d5
| Field | From #1177 | To #1817 |
|---|
| mathlib.module | Mathlib.Algebra.Polynomial.RingDivision | Mathlib.Algebra.Polynomial.Div |
modifiedEigenspace of a matrix8f6b1cbef8f3
| Field | From #1177 | To #1817 |
|---|
| note | `eigenspace` applied to `Matrix.toLin'`; e.g. `iSup_eigenspace_toLin'_diagonal_eq_top`. | `eigenspace` applied to `Matrix.toLin'`; e.g. `Matrix.iSup_eigenspace_toLin'_diagonal_eq_top`. |
modifiedGeometric multiplicity846f11b9e70e
| Field | From #1177 | To #1817 |
|---|
| mathlib.decl | Module.finrank | Module.End.eigenspace |
modifiedEigenbasis from total geometric multiplicity2c2bf355d5af
| Field | From #1177 | To #1817 |
|---|
| note | For semisimple endomorphisms over an algebraically closed field the eigenspaces span; combined with `eigenspaces_iSupIndep` they form a direct sum decomposition. | For semisimple endomorphisms the eigenspaces span; combined with `eigenspaces_iSupIndep` they form a direct sum decomposition. |
modifiedDeterminant equals product of eigenvalues95583262f462
| Field | From #1177 | To #1817 |
|---|
| note | Also `Matrix.det_eq_prod_roots_charpoly` for algebraically closed fields. | Determinant is the product of charpoly roots when it splits. |
modifiedDefiniteness gives sign of eigenvalues133eeb37e571
| Field | From #1177 | To #1817 |
|---|
| note | `PosSemidef.eigenvalues_nonneg` and `IsHermitian.posSemidef_iff_eigenvalues_nonneg` cover the positive case. | `PosSemidef.eigenvalues_nonneg` covers the positive case. |
modifiedUnitary matrix eigenvalues have absolute value one06ff04121a14
| Field | From #1177 | To #1817 |
|---|
| mathlib.decl | Unitary.spectrum_subset_circle | spectrum.norm_eq_one_of_unitary |
| note | `Unitary.spectrum_subset_circle` and `spectrum.norm_eq_one_of_unitary` give |λ|=1 for unitary elements in C*-algebras, applying to unitary matrices. | `spectrum.norm_eq_one_of_unitary` and `Unitary.spectrum_subset_circle` give |λ|=1 for unitary elements in C*-algebras, applying to unitary matrices. |
modifiedDefective matrix and Jordan normal form52f3757be9c0
| Field | From #1177 | To #1817 |
|---|
| mathlib.module | Mathlib.LinearAlgebra.JordanChevalley | Mathlib.LinearAlgebra.Eigenspace.Basic |
| note | Generalized eigenspaces and `JordanChevalley` decomposition exist; full Jordan normal form and `defective` predicate are not formalized. | Generalized eigenspaces exist and Jordan–Chevalley decomposition is formalized; full Jordan normal form and `defective` predicate are not. |
modifiedDiagonal matrix example65e3b5a11aaf
| Field | From #1177 | To #1817 |
|---|
| mathlib.decl | Matrix.spectrum_diagonal | spectrum_diagonal |
| note | `spectrum_diagonal` shows `spectrum R (diagonal d) = Set.range d`. | `spectrum_diagonal` shows `spectrum R (Matrix.diagonal d) = Set.range d`. |
modifiedGeometric multiplicity (general)481dd30ed58c
| Field | From #1177 | To #1817 |
|---|
| mathlib.decl | Module.finrank | Module.End.eigenspace |
modifiedAbel–Ruffini limits explicit eigenvalue formulas1ea850c3750b
| Field | From #1177 | To #1817 |
|---|
| mathlib.decl | not_solvable_by_rad | isSolvable_gal_of_irreducible |
| note | Abel–Ruffini is formalized for polynomials; not specialized to eigenvalues. | Abel–Ruffini (`isSolvable_gal_of_irreducible`) is formalized for polynomials; not specialized to eigenvalues. |
addedEigenvectors of different eigenvalues are linearly independent6944762ed5e9
addedAt most n distinct eigenvalues in dimension n34e9947f1947
addedEigenvalues of the inverse are reciprocals00ffc4baf231
addedReal symmetric matrices have real eigenvalues6f56152a60d5