Theorem Module.End.maxGenEigenspace_eq_maxGenEigenspace_zero

Modification history

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