Theorem Module.End.exists_eigenvalue

Modification history

2023-06-10 05:46
Mathlib/LinearAlgebra/Eigenspace/IsAlgClosed.lean
feat: port LinearAlgebra.Eigenspace.IsAlgClosed (#4943)
Added Module.End.exists_eigenvalueView on Github →