feat: port GroupTheory.Perm.Support (#1614)

Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com> Co-authored-by: Moritz Firsching <firsching@google.com>
leanprover-community · Jan 17, 2023 · 4b7c58f · 4b7c58f
1 parent 86d0135
commit 4b7c58f
Show file tree

Hide file tree

Showing 2 changed files with 675 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -455,6 +455,7 @@ import Mathlib.GroupTheory.GroupAction.Sum
 import Mathlib.GroupTheory.GroupAction.Support
 import Mathlib.GroupTheory.GroupAction.Units
 import Mathlib.GroupTheory.Perm.Basic
+import Mathlib.GroupTheory.Perm.Support
 import Mathlib.GroupTheory.Perm.ViaEmbedding
 import Mathlib.GroupTheory.Submonoid.Basic
 import Mathlib.GroupTheory.Submonoid.Center