fix(Subsemigroup/Operations): fix types (#9716)

Fix theorem statements of `AddSubsemigroup.toSubsemigroup'_closure` and `Subsemigroup.toAddSubsemigroup'_closure`.
leanprover-community · Jan 14, 2024 · d73146f · d73146f
1 parent ebe630d
commit d73146f
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Mathlib/GroupTheory/Subsemigroup/Operations.lean b/Mathlib/GroupTheory/Subsemigroup/Operations.lean
@@ -109,7 +109,7 @@ theorem Subsemigroup.toAddSubsemigroup_closure (S : Set M) :
 
 theorem AddSubsemigroup.toSubsemigroup'_closure (S : Set (Additive M)) :
     AddSubsemigroup.toSubsemigroup' (AddSubsemigroup.closure S) =
-      Subsemigroup.closure (Multiplicative.ofAdd ⁻¹' S) :=
+      Subsemigroup.closure (Additive.ofMul ⁻¹' S) :=
   le_antisymm
     (AddSubsemigroup.toSubsemigroup'.le_symm_apply.1 <|
       AddSubsemigroup.closure_le.2 (Subsemigroup.subset_closure (M := M)))
@@ -156,7 +156,7 @@ theorem AddSubsemigroup.toSubsemigroup_closure (S : Set A) :
 
 theorem Subsemigroup.toAddSubsemigroup'_closure (S : Set (Multiplicative A)) :
     Subsemigroup.toAddSubsemigroup' (Subsemigroup.closure S) =
-    AddSubsemigroup.closure (Additive.ofMul ⁻¹' S) :=
+      AddSubsemigroup.closure (Multiplicative.ofAdd ⁻¹' S) :=
   le_antisymm
     (Subsemigroup.toAddSubsemigroup'.to_galoisConnection.l_le <|
       Subsemigroup.closure_le.2 <| AddSubsemigroup.subset_closure (M := A))