Clean up imports

Geoc2022 · Geoc2022 · commit caf3d2a4597b · 2026-01-08T22:25:23.000-05:00
diff --git a/Game/Levels/GroupExamples/L01_Z_mod_mZ_Id.lean b/Game/Levels/GroupExamples/L01_Z_mod_mZ_Id.lean
@@ -1,5 +1,5 @@
 import Game.MyAlgebra.Z_mod_mZ
-import Game.Levels.Group.L08_InvInv
+import Game.Levels.Group
 
 World "Group Examples"
 Level 1
diff --git a/Game/MyAlgebra/Subgroup_Def.lean b/Game/MyAlgebra/Subgroup_Def.lean
@@ -1,4 +1,4 @@
-import Game.Levels.Group.L11_InvInv
+import Game.Levels.Group
 
 namespace MyAlgebra
 

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-import Game.Levels.Group.L11_InvInv`
	`1`	`+import Game.Levels.Group`
`2`	`2`
`3`	`3`	`namespace MyAlgebra`
`4`	`4`