Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-02 11:43 cd36773a

View on Github →

feat(linear_algebra/eigenspace): add generalized eigenspaces (#4015) Add the definition of generalized eigenspaces, eigenvectors and eigenvalues. Add some basic lemmas about them. Another step towards #3864.

Estimated changes

Modified src/algebra/group_power.lean

added theorem nsmul_add_sub_nsmul

added theorem pow_mul_pow_sub

added theorem pow_sub_mul_pow

added theorem sub_nsmul_nsmul_add

Modified src/linear_algebra/eigenspace.lean

added theorem module.End.eigenspace_le_generalized_eigenspace

added theorem module.End.exp_ne_zero_of_has_generalized_eigenvalue

added def module.End.generalized_eigenspace

added theorem module.End.generalized_eigenspace_mono

added def module.End.has_generalized_eigenvalue

added theorem module.End.has_generalized_eigenvalue_of_has_eigenvalue

added theorem module.End.has_generalized_eigenvalue_of_has_generalized_eigenvalue_of_le

added def module.End.has_generalized_eigenvector