Update Mathlib/GroupTheory/QuotientGroup/Basic.lean

Co-authored-by: Thomas Browning <[email protected]>

Mathlib/GroupTheory/QuotientGroup/Basic.lean

@@ -342,7 +342,7 @@ theorem comap_map_mk' (N H : Subgroup G) [N.Normal] :
   or fourth isomorphism theorem for multiplicative groups-/
 @[to_additive "The **correspondence theorem**, or lattice theorem,
   or fourth isomorphism theorem for additive groups"]
-def comap_mk'_OrderIso (N : Subgroup G) [hn : N.Normal] :
+def comapMk'OrderIso (N : Subgroup G) [hn : N.Normal] :
     Subgroup (G ⧸ N) ≃o { H : Subgroup G // N ≤ H } where
   toFun H' := ⟨Subgroup.comap (mk' N) H', le_comap_mk' N _⟩
   invFun H := Subgroup.map (mk' N) H