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.
feat(Algebra/Lie/Weights/Basic): define weightSpace
(#18660)
Before this, mathlib only had genWeightSpace
which takes maximal
generalized eigenspaces instead of "ordinary" eigenspaces.