feat: Fitting decomposition of a representation of a nilpotent Lie al…

…gebra (#7556)
leanprover-community · Oct 11, 2023 · 2c0ab8d · 2c0ab8d
1 parent c00742d
commit 2c0ab8d
Show file tree

Hide file tree

Showing 3 changed files with 446 additions and 278 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -285,7 +285,8 @@ import Mathlib.Algebra.Lie.Subalgebra
 import Mathlib.Algebra.Lie.Submodule
 import Mathlib.Algebra.Lie.TensorProduct
 import Mathlib.Algebra.Lie.UniversalEnveloping
-import Mathlib.Algebra.Lie.Weights
+import Mathlib.Algebra.Lie.Weights.Basic
+import Mathlib.Algebra.Lie.Weights.Cartan
 import Mathlib.Algebra.LinearRecurrence
 import Mathlib.Algebra.ModEq
 import Mathlib.Algebra.Module.Algebra