-
Notifications
You must be signed in to change notification settings - Fork 234
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: IsUnit if exists both inverses #10719
Conversation
line too long
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Changed proof using left_inv_eq_right_inv
Spaces Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: damiano <adomani@gmail.com>
Co-authored-by: damiano <adomani@gmail.com>
Please merge master and make sure this lemma is next to the one added in #10832 |
I really don't know how to merge master... |
@XavierXarles, I took care of merging master, moving the lemma and adding to doc-strings: I hope that you do not mind! For future reference, if you use Git from the commandline, "merging master" likely looks as follows: git fetch
git merge origin/master
## maybe fix conflicts -- there were none this time |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors merge
Thanks!
Added one theorem Co-authored-by: Xavier Xarles <56635243+XavierXarles@users.noreply.github.com> Co-authored-by: adomani <adomani@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Added one theorem Co-authored-by: Xavier Xarles <56635243+XavierXarles@users.noreply.github.com> Co-authored-by: adomani <adomani@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Added one theorem Co-authored-by: Xavier Xarles <56635243+XavierXarles@users.noreply.github.com> Co-authored-by: adomani <adomani@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Added one theorem Co-authored-by: Xavier Xarles <56635243+XavierXarles@users.noreply.github.com> Co-authored-by: adomani <adomani@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Added one theorem Co-authored-by: Xavier Xarles <56635243+XavierXarles@users.noreply.github.com> Co-authored-by: adomani <adomani@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Added one theorem Co-authored-by: Xavier Xarles <56635243+XavierXarles@users.noreply.github.com> Co-authored-by: adomani <adomani@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Added one theorem