Theorem Module.End.mem_iInf_maxGenEigenspace_iff

Modification history

2024-10-17 08:31
Mathlib/LinearAlgebra/Eigenspace/Pi.lean
feat: generalise `LieModule.independent_genWeightSpace` to any family of compatible endomorphisms (#17654) …
Added Module.End.mem_iInf_maxGenEigenspace_iffView on Github →