Commit 2020-09-06 12:14 1117ae79

View on Github →

feat(linear_algebra): Add lemmas about powers of endomorphisms (#4036) Add lemmas about powers of endomorphisms and the corollary that every generalized eigenvector is a generalized eigenvector for exponent findim K V.

Estimated changes

Modified src/linear_algebra/eigenspace.lean

added theorem module.End.generalized_eigenspace_eq_generalized_eigenspace_findim_of_le

added theorem module.End.generalized_eigenspace_le_generalized_eigenspace_findim

Modified src/linear_algebra/finite_dimensional.lean

added theorem module.End.exists_ker_pow_eq_ker_pow_succ

added theorem module.End.ker_pow_constant

added theorem module.End.ker_pow_eq_ker_pow_findim_of_le

added theorem module.End.ker_pow_le_ker_pow_findim

added theorem submodule.findim_lt_findim_of_lt