mathlib3
af53c9d7
- chore(algebra/ring): move some classes to `group_with_zero` (#3232)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
chore(algebra/ring): move some classes to `group_with_zero` (#3232) Move `nonzero`, `mul_zero_class` and `no_zero_divisors` to `group_with_zero`: these classes don't need `(+)`.
Author
urkud
Parents
da481e77
Loading