Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-24 03:33 ef18740b

View on Github →

feat(linear_algebra/eigenspace): generalized eigenvectors span the entire space (#4111)

Estimated changes

Modified docs/references.bib

Modified src/linear_algebra/basic.lean

added theorem linear_map.ker_restrict

Modified src/linear_algebra/eigenspace.lean

modified theorem module.End.aeval_apply_of_has_eigenvector

modified def module.End.eigenspace

modified theorem module.End.eigenspace_aeval_polynomial_degree_1

modified theorem module.End.eigenspace_div

modified theorem module.End.eigenspace_le_generalized_eigenspace

modified theorem module.End.eigenvectors_linear_independent

modified theorem module.End.exists_eigenvalue

modified theorem module.End.exp_ne_zero_of_has_generalized_eigenvalue

added def module.End.generalized_eigenrange

modified def module.End.generalized_eigenspace

modified theorem module.End.generalized_eigenspace_eq_generalized_eigenspace_findim_of_le

modified theorem module.End.generalized_eigenspace_mono

modified theorem module.End.generalized_eigenspace_restrict

added theorem module.End.generalized_eigenvec_disjoint_range_ker

modified def module.End.has_eigenvalue

modified def module.End.has_eigenvector

modified def module.End.has_generalized_eigenvalue

modified theorem module.End.has_generalized_eigenvalue_of_has_eigenvalue

modified theorem module.End.has_generalized_eigenvalue_of_has_generalized_eigenvalue_of_le

modified def module.End.has_generalized_eigenvector

modified theorem module.End.ker_aeval_ring_hom'_unit_polynomial

added theorem module.End.map_generalized_eigenrange_le

modified theorem module.End.mem_eigenspace_iff

added theorem module.End.pos_findim_generalized_eigenspace_of_has_eigenvalue

added theorem module.End.supr_generalized_eigenspace_eq_top

Modified src/ring_theory/algebra.lean

added theorem algebra.mul_sub_algebra_map_commutes

added theorem algebra.mul_sub_algebra_map_pow_commutes