Commit 2023-06-08 10:38 2b1f0dcc

View on Github →

feat: port LinearAlgebra.Eigenspace.Basic (#4842) Two instances defined in Data.Dfinsupp.Basic are used in this file (with explicit arguments) so I gave them names.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Dfinsupp/Basic.lean

Created Mathlib/LinearAlgebra/Eigenspace/Basic.lean

added def Module.End.Eigenvalues

added theorem Module.End.HasEigenvalue.exists_hasEigenvector

added def Module.End.HasEigenvalue

added theorem Module.End.HasEigenvector.apply_eq_smul

added def Module.End.HasEigenvector

added def Module.End.HasGeneralizedEigenvalue

added def Module.End.HasGeneralizedEigenvector

added def Module.End.eigenspace

added theorem Module.End.eigenspace_div

added theorem Module.End.eigenspace_le_generalizedEigenspace

added theorem Module.End.eigenspace_restrict_eq_bot

added theorem Module.End.eigenspace_restrict_le_eigenspace

added theorem Module.End.eigenspace_zero

added theorem Module.End.eigenspaces_independent

added theorem Module.End.eigenvectors_linearIndependent

added theorem Module.End.exp_ne_zero_of_hasGeneralizedEigenvalue

added def Module.End.generalizedEigenrange

added def Module.End.generalizedEigenspace

added theorem Module.End.generalizedEigenspace_eq_generalizedEigenspace_finrank_of_le

added theorem Module.End.generalizedEigenspace_le_generalizedEigenspace_finrank

added theorem Module.End.generalizedEigenspace_le_maximal

added theorem Module.End.generalizedEigenspace_restrict

added theorem Module.End.generalizedEigenspace_zero

added theorem Module.End.generalized_eigenvec_disjoint_range_ker

added theorem Module.End.hasEigenvalue_iff_mem_spectrum

added theorem Module.End.hasEigenvalue_of_hasEigenvector

added theorem Module.End.hasEigenvalue_of_hasGeneralizedEigenvalue

added theorem Module.End.hasGeneralizedEigenvalue_iff_hasEigenvalue

added theorem Module.End.hasGeneralizedEigenvalue_of_hasEigenvalue

added theorem Module.End.hasGeneralizedEigenvalue_of_hasGeneralizedEigenvalue_of_le

added theorem Module.End.map_generalizedEigenrange_le

added def Module.End.maximalGeneralizedEigenspace

added theorem Module.End.maximalGeneralizedEigenspace_eq

added theorem Module.End.mem_eigenspace_iff

added theorem Module.End.mem_generalizedEigenspace

added theorem Module.End.mem_maximalGeneralizedEigenspace

added theorem Module.End.mem_spectrum_of_hasEigenvalue

added theorem Module.End.pos_finrank_generalizedEigenspace_of_hasEigenvalue