feat: port Algebra.Lie.Nilpotent (#4919)

leanprover-community · Jun 9, 2023 · fdc28c9 · fdc28c9
1 parent 8907994
commit fdc28c9
Show file tree

Hide file tree

Showing 2 changed files with 751 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -217,6 +217,7 @@ import Mathlib.Algebra.Lie.DirectSum
 import Mathlib.Algebra.Lie.Free
 import Mathlib.Algebra.Lie.IdealOperations
 import Mathlib.Algebra.Lie.Matrix
+import Mathlib.Algebra.Lie.Nilpotent
 import Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra
 import Mathlib.Algebra.Lie.Normalizer
 import Mathlib.Algebra.Lie.OfAssociative