Skip to content

Commit 4b7c58f

Browse files
mo271ChrisHughes24
andcommitted
feat: port GroupTheory.Perm.Support (#1614)
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com> Co-authored-by: Moritz Firsching <firsching@google.com>
1 parent 86d0135 commit 4b7c58f

File tree

2 files changed

+675
-0
lines changed

2 files changed

+675
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -455,6 +455,7 @@ import Mathlib.GroupTheory.GroupAction.Sum
455455
import Mathlib.GroupTheory.GroupAction.Support
456456
import Mathlib.GroupTheory.GroupAction.Units
457457
import Mathlib.GroupTheory.Perm.Basic
458+
import Mathlib.GroupTheory.Perm.Support
458459
import Mathlib.GroupTheory.Perm.ViaEmbedding
459460
import Mathlib.GroupTheory.Submonoid.Basic
460461
import Mathlib.GroupTheory.Submonoid.Center

0 commit comments

Comments
 (0)