mathlib3
feat(algebra/group_with_zero): groups with a zero element adjoined
#2242
Merged
Merged
feat(algebra/group_with_zero): groups with a zero element adjoined #2242
mergify
merged
24 commits into
master
from
group-with-zero-refactor
feat(algebra/group_with_zero*): Basics on groups with a zero adjoined
fde11a8c
feat(algebra/group_with_zero*): Basics on groups with a zero adjoined
dcd80961
Merge branch 'group-with-zero-oops' into group-with-zero-refactor
9b61f62a
Make argument implicit
48f5662d
Move inv_eq_zero out of gwz namespace
b8f87772
Partial refactor
b2603f4a
Remove open_locale classical
c2c7116e
Fix build
a357d522
Factor out monoid_with_zero
8d805c1e
Fix linter errors, hopefully
df4259e6
Fix build
c611a214
Fix tests
908f8f1a
kim-em
commented
on 2020-03-27
kim-em
commented
on 2020-03-27
Replace G with G0
46f4818b
Add spaces around `^`
f60f477d
Add spaces and backticks in docstrings
a18a1ec7
Fix docstring of `mk0`
906837e6
Fix statement of inv_eq_iff
3f5dc1a6
Golf inv_injective
d838fc1d
Golf inv_eq_zero
857a69a3
kim-em
commented
on 2020-03-27
kim-em
commented
on 2020-03-27
kim-em
commented
on 2020-03-27
kim-em
commented
on 2020-03-27
kim-em
commented
on 2020-03-27
Remove the gwz namespace
20852be9
kim-em
approved these changes
on 2020-04-04
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into group-with-zero-refactor
d94b4ec6
Fix build
7ae0def5
Merge master
ac3b3bdf
Merge branch 'master' into group-with-zero-refactor
515411f3
Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub