Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-07 06:47 6b016921

View on Github →

chore(linear_algebra/eigenspace): split file (#19163)

Estimated changes

Modified src/algebra/lie/nilpotent.lean

Modified src/algebra/lie/weights.lean

Modified src/analysis/inner_product_space/rayleigh.lean

Modified src/analysis/inner_product_space/spectrum.lean

Renamed src/linear_algebra/eigenspace.lean to src/linear_algebra/eigenspace/basic.lean

deleted theorem module.End.aeval_apply_of_has_eigenvector

deleted theorem module.End.eigenspace_aeval_polynomial_degree_1

deleted theorem module.End.exists_eigenvalue

deleted theorem module.End.has_eigenvalue_iff_is_root

deleted theorem module.End.has_eigenvalue_of_is_root

deleted theorem module.End.is_root_of_has_eigenvalue

deleted theorem module.End.ker_aeval_ring_hom'_unit_polynomial

deleted theorem module.End.supr_generalized_eigenspace_eq_top

Created src/linear_algebra/eigenspace/is_alg_closed.lean

added theorem module.End.exists_eigenvalue

added theorem module.End.supr_generalized_eigenspace_eq_top

Created src/linear_algebra/eigenspace/minpoly.lean

added theorem module.End.aeval_apply_of_has_eigenvector

added theorem module.End.eigenspace_aeval_polynomial_degree_1

added theorem module.End.has_eigenvalue_iff_is_root

added theorem module.End.has_eigenvalue_of_is_root

added theorem module.End.is_root_of_has_eigenvalue

added theorem module.End.ker_aeval_ring_hom'_unit_polynomial