Theorem Module.End.iSup_genEigenspace_eq_genEigenspace_finrank

Modification history

2024-10-25 20:58

Mathlib/LinearAlgebra/Eigenspace/Basic.lean

chore(LinearAlgebra): use maxGenEigenspace instead of iSup over genEigenspace (#18037)

Deleted Module.End.iSup_genEigenspace_eq_genEigenspace_finrank View on Github →

2024-05-21 19:30

Mathlib/LinearAlgebra/Eigenspace/Basic.lean

chore(Algebra,LinearAlgebra): shorten names of generalizedEigenspace and maximalGeneralizedEigenspace (#13078) …

Added Module.End.iSup_genEigenspace_eq_genEigenspace_finrank View on Github →