Commit 2023-11-08 18:36 7fbfeaf5

View on Github →

feat: generalized eigenspaces are independent (#8177) The main change is to upgrade the existing Module.End.eigenspaces_independent, which applied only to eigenspaces (and required a [Field K] assumption) to Module.End.independent_generalizedEigenspace, which applies to generalized eigenspaces (and requires only [NoZeroSMulDivisors R M])

Estimated changes

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

added theorem Module.End.disjoint_generalizedEigenspace

added theorem Module.End.disjoint_iSup_generalizedEigenspace

modified theorem Module.End.eigenspaces_independent

modified theorem Module.End.eigenvectors_linearIndependent

added theorem Module.End.iSup_generalizedEigenspace_eq_generalizedEigenspace_finrank

added theorem Module.End.independent_generalizedEigenspace

added theorem Module.End.injOn_generalizedEigenspace

added theorem Module.End.mapsTo_generalizedEigenspace_of_comm

added theorem Module.End.mapsTo_iSup_generalizedEigenspace_of_comm

added theorem Submodule.inf_generalizedEigenspace

Modified Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean

added theorem Module.End.finite_hasEigenvalue