Commit 2024-11-05 21:51 e09ea4be

View on Github →

feat(Algebra/Lie/Weights/Basic): define weightSpace (#18660) Before this, mathlib only had genWeightSpace which takes maximal generalized eigenspaces instead of "ordinary" eigenspaces.

Estimated changes