Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-06-15 06:12
15656ac1
View on Github →
feat: port Analysis.InnerProductSpace.Spectrum (
#5058
)
depends on:
#4920
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Analysis/InnerProductSpace/Spectrum.lean
added
theorem
LinearMap.IsSymmetric.apply_eigenvectorBasis
added
theorem
LinearMap.IsSymmetric.conj_eigenvalue_eq_self
added
theorem
LinearMap.IsSymmetric.diagonalization_apply_self_apply
added
theorem
LinearMap.IsSymmetric.diagonalization_symm_apply
added
theorem
LinearMap.IsSymmetric.directSum_decompose_apply
added
theorem
LinearMap.IsSymmetric.direct_sum_isInternal
added
theorem
LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply
added
theorem
LinearMap.IsSymmetric.hasEigenvalue_eigenvalues
added
theorem
LinearMap.IsSymmetric.hasEigenvector_eigenvectorBasis
added
theorem
LinearMap.IsSymmetric.invariant_orthogonalComplement_eigenspace
added
theorem
LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces
added
theorem
LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot'
added
theorem
LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot
added
theorem
LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_invariant
added
theorem
LinearMap.IsSymmetric.orthogonalFamily_eigenspaces'
added
theorem
LinearMap.IsSymmetric.orthogonalFamily_eigenspaces
added
theorem
eigenvalue_nonneg_of_nonneg
added
theorem
eigenvalue_pos_of_pos
added
theorem
inner_product_apply_eigenvector
Modified
Mathlib/LinearAlgebra/Eigenspace/Basic.lean
added
def
Module.End.Eigenvalues.val