Commit 2023-11-30 16:55 125ea267

View on Github →

feat: existence of simultaneous eigenvectors given simultaneous generalized eigenvectors for Lie modules (#8745)

Estimated changes

Modified Mathlib/Algebra/Lie/Weights/Linear.lean

added theorem LieModule.exists_forall_lie_eq_smul_of_weightSpace_ne_bot

modified def LieModule.shiftedWeightSpace.shift