Theorem LinearMap.finrank_eigenspace_le

Modification history

2025-09-16 12:06
Mathlib/LinearAlgebra/Eigenspace/Zero.lean
feat: generalize `LinearMap.finrank_maxGenEigenspace` (#29428)
Added LinearMap.finrank_eigenspace_leView on Github →