Zulip Chat Archive
Stream: maths
Topic: duplicate is_group_hom
Johan Commelin (Feb 11 2019 at 11:49):
I think these are duplicates.
https://github.com/leanprover-community/mathlib/blob/master/src/group_theory/quotient_group.lean#L50
https://github.com/leanprover-community/mathlib/blob/master/src/group_theory/quotient_group.lean#L82
Johan Commelin (Feb 11 2019 at 11:50):
@Chris Hughes You can probably fix this faster than I can create a PR (-;
Last updated: Dec 20 2023 at 11:08 UTC