From d5bd1c7673d608da6334404e6d0cb5c4cf9c2028 Mon Sep 17 00:00:00 2001 From: Hannah Fechtner <123216642+hannahfechtner@users.noreply.github.com> Date: Thu, 31 Oct 2024 12:14:36 -0400 Subject: [PATCH] capitalization 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 ab6c01905ae41..222b446bd5d38 100644 --- a/Mathlib/GroupTheory/Congruence/Basic.lean +++ b/Mathlib/GroupTheory/Congruence/Basic.lean @@ -86,7 +86,7 @@ theorem conGen_le_comap {M N : Type*} [Mul M] [Mul N] (f : M → N) (.mul h1 h2))) h @[to_additive] -theorem comap_conGen_of_Bijective {M N : Type*} [Mul M] [Mul N] (f : M → N) +theorem comap_conGen_of_bijective {M N : Type*} [Mul M] [Mul N] (f : M → N) (hf : Function.Bijective f) (H : ∀ (x y : M), f (x * y) = f x * f y) (rel : N → N → Prop) : Con.comap f H (conGen rel) = conGen (fun x y ↦ rel (f x) (f y)) := by apply le_antisymm _ (conGen_le_comap f H rel)