Skip to content

Commit

Permalink
capitalization
Browse files Browse the repository at this point in the history
Co-authored-by: Yaël Dillies <[email protected]>
  • Loading branch information
hannahfechtner and YaelDillies authored Oct 31, 2024
1 parent c2c0709 commit d5bd1c7
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/GroupTheory/Congruence/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down

0 comments on commit d5bd1c7

Please sign in to comment.