mathlib3
929c9018
- refactor(ring_theory/*): Remove unnecessary commutativity assumptions (#13966)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
refactor(ring_theory/*): Remove unnecessary commutativity assumptions (#13966) This replaces `[comm_ring R]` or `[comm_semiring R]` with `[ring R]` or `[semiring R]`, without changing any proofs.
Author
haruhisa-enomoto
Parents
8e0ab168
Loading