From 80d98a95fc5c4bd072ff93e268ac6b7c25942f55 Mon Sep 17 00:00:00 2001 From: Johannes Choo Date: Mon, 6 Jan 2025 09:00:16 +0800 Subject: [PATCH] Update Mathlib/GroupTheory/QuotientGroup/Basic.lean Co-authored-by: Thomas Browning --- Mathlib/GroupTheory/QuotientGroup/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/GroupTheory/QuotientGroup/Basic.lean b/Mathlib/GroupTheory/QuotientGroup/Basic.lean index 4ce230e0c8565..fd4ad245f5e68 100644 --- a/Mathlib/GroupTheory/QuotientGroup/Basic.lean +++ b/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