Mathlib v3 is deprecated. Go to Mathlib v4

Theorem module.End.supr_generalized_eigenspace_eq_top

Modification history

2023-06-07 06:47

src/linear_algebra/eigenspace/basic.lean

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

Modified module.End.supr_generalized_eigenspace_eq_top View on Github →

2020-09-24 03:33

src/linear_algebra/eigenspace.lean

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

Added module.End.supr_generalized_eigenspace_eq_top View on Github →