Commit 2023-06-15 07:21 aee56e09

View on Github →

feat: port LinearAlgebra.Matrix.Spectrum (#5059)

depends on: #4920
depends on: #5058

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/Spectrum.lean

added theorem Matrix.IsHermitian.conjTranspose_eigenvectorMatrix

added theorem Matrix.IsHermitian.conjTranspose_eigenvectorMatrixInv

added theorem Matrix.IsHermitian.det_eq_prod_eigenvalues

added theorem Matrix.IsHermitian.eigenvalues_eq

added theorem Matrix.IsHermitian.eigenvectorMatrixInv_apply

added theorem Matrix.IsHermitian.eigenvectorMatrix_apply

added theorem Matrix.IsHermitian.eigenvectorMatrix_mul_inv

added theorem Matrix.IsHermitian.spectral_theorem