mathlib
7e307bcc
- chore(algebra/ring): delete a duplicate instance (#5215)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
chore(algebra/ring): delete a duplicate instance (#5215) In #3303 and #3296 which were merged 1 day apart two versions of the instance comm_monoid_with_zero from a comm_semiring were added 5 lines apart in the file, delete one.
Author
alexjbest
Parents
2d00ba48
Loading