Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-06 18:32 6ea4e9b1

View on Github →

feat(linear_algebra/eigenspace): generalized eigenvalues are just eigenvalues (#7059)

Estimated changes

Modified src/linear_algebra/eigenspace.lean

modified theorem module.End.generalized_eigenspace_mono

added theorem module.End.has_eigenvalue_of_has_generalized_eigenvalue

added theorem module.End.has_generalized_eigenvalue_iff_has_eigenvalue