Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

feat(algebra/group/basic.lean): add inv_mul_eq_one#2349

Merged
mergify[bot] merged 2 commits into
masterfrom
inv_mul_eq_one
Apr 7, 2020
Merged

feat(algebra/group/basic.lean): add inv_mul_eq_one#2349
mergify[bot] merged 2 commits into
masterfrom
inv_mul_eq_one

Conversation

@kbuzzard
Copy link
Copy Markdown
Member

@kbuzzard kbuzzard commented Apr 7, 2020

TO CONTRIBUTORS:

Make sure you have:

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

@kim-em kim-em added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Apr 7, 2020
@mergify mergify Bot merged commit 0e2970c into master Apr 7, 2020
@mergify mergify Bot deleted the inv_mul_eq_one branch April 7, 2020 22:38
butterthebuddha pushed a commit to butterthebuddha/mathlib that referenced this pull request May 15, 2020
…ity#2349)

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
butterthebuddha pushed a commit to butterthebuddha/mathlib that referenced this pull request May 16, 2020
…ity#2349)

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
cipher1024 pushed a commit to cipher1024/mathlib that referenced this pull request Mar 15, 2022
…ity#2349)

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants