From 10bdf06f3bf449289b1009bfe22e4a32be3938ec Mon Sep 17 00:00:00 2001 From: Hannah Fechtner <123216642+hannahfechtner@users.noreply.github.com> Date: Thu, 31 Oct 2024 12:15:02 -0400 Subject: [PATCH] name change MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Yaël Dillies --- Mathlib/GroupTheory/Congruence/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/GroupTheory/Congruence/Basic.lean b/Mathlib/GroupTheory/Congruence/Basic.lean index 222b446bd5d38..d15a453853872 100644 --- a/Mathlib/GroupTheory/Congruence/Basic.lean +++ b/Mathlib/GroupTheory/Congruence/Basic.lean @@ -74,7 +74,7 @@ theorem congr_mk {c d : Con M} (h : c = d) (a : M) : Con.congr h (a : c.Quotient) = (a : d.Quotient) := rfl @[to_additive] -theorem conGen_le_comap {M N : Type*} [Mul M] [Mul N] (f : M → N) +theorem le_comap_conGen {M N : Type*} [Mul M] [Mul N] (f : M → N) (H : ∀ (x y : M), f (x * y) = f x * f y) (rel : N → N → Prop) : conGen (fun x y ↦ rel (f x) (f y)) ≤ Con.comap f H (conGen rel) := by intro x y h