Skip to content

Commit

Permalink
fix(algebra/group/hom): Fix spurrious arguments (#1581)
Browse files Browse the repository at this point in the history
This bug was introduced in eb230d3
  • Loading branch information
PatrickMassot authored and mergify[bot] committed Oct 21, 2019
1 parent f19dbf2 commit 6cf3d04
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions src/algebra/group/hom.lean
Original file line number Diff line number Diff line change
Expand Up @@ -38,8 +38,8 @@ as `map_mul`; a separate constructor `monoid_hom.mk'` will construct
group homs (i.e. monoid homs between groups) given only a proof
that multiplication is preserved,
Throughout the `monoid_hom` section implicit `{}` brackets are often used instead of type class `[]` brackets.
This is done when the instances can be inferred because they are implicit arguments to the type `monoid_hom`.
Throughout the `monoid_hom` section implicit `{}` brackets are often used instead of type class `[]` brackets.
This is done when the instances can be inferred because they are implicit arguments to the type `monoid_hom`.
When they can be inferred from the type it is faster to use this method than to use type class inference.
## Tags
Expand Down Expand Up @@ -293,12 +293,12 @@ instance (f : M →* N) : is_monoid_hom (f : M → N) :=
{ map_mul := f.map_mul,
map_one := f.map_one }

omit mN mM

@[to_additive is_add_group_hom]
instance (f : G →* H) : is_group_hom (f : G → H) :=
{ map_mul := f.map_mul }

omit mN mM

/-- The identity map from a monoid to itself. -/
@[to_additive]
def id (M : Type*) [monoid M] : M →* M :=
Expand Down

0 comments on commit 6cf3d04

Please sign in to comment.