refactor: rename FreeProduct to Monoid.CoprodI (#6055)

leanprover-community · Aug 2, 2023 · a70e9fd · a70e9fd
1 parent 571c23b
commit a70e9fd
Show file tree

Hide file tree

Showing 2 changed files with 172 additions and 162 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1945,6 +1945,7 @@ import Mathlib.GroupTheory.Commutator
 import Mathlib.GroupTheory.CommutingProbability
 import Mathlib.GroupTheory.Complement
 import Mathlib.GroupTheory.Congruence
+import Mathlib.GroupTheory.CoprodI
 import Mathlib.GroupTheory.Coset
 import Mathlib.GroupTheory.Divisible
 import Mathlib.GroupTheory.DoubleCoset
@@ -1955,7 +1956,6 @@ import Mathlib.GroupTheory.Finiteness
 import Mathlib.GroupTheory.FreeAbelianGroup
 import Mathlib.GroupTheory.FreeAbelianGroupFinsupp
 import Mathlib.GroupTheory.FreeGroup
-import Mathlib.GroupTheory.FreeProduct
 import Mathlib.GroupTheory.GroupAction.Basic
 import Mathlib.GroupTheory.GroupAction.BigOperators
 import Mathlib.GroupTheory.GroupAction.ConjAct