Skip to content

Commit

Permalink
chore: fix bad name of instance (#1903)
Browse files Browse the repository at this point in the history
  • Loading branch information
jcommelin committed Jan 28, 2023
1 parent 2c6b1ac commit 0985cf5
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Hom/GroupInstances.lean
Expand Up @@ -53,7 +53,7 @@ instance MonoidHom.commMonoid [MulOneClass M] [CommMonoid N] :
@[to_additive AddMonoidHom.addCommGroup
"If `G` is an additive commutative group, then `M →+ G` is an additive commutative
group too."]
instance commGroup {M G} [MulOneClass M] [CommGroup G] : CommGroup (M →* G) :=
instance MonoidHom.commGroup {M G} [MulOneClass M] [CommGroup G] : CommGroup (M →* G) :=
{ MonoidHom.commMonoid with
inv := Inv.inv,
div := Div.div,
Expand Down

0 comments on commit 0985cf5

Please sign in to comment.