mathlib3
33ed7d33
- chore(data/polynomial/field_division): remove `polynomial.div` and `polynomial.mod`
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
chore(data/polynomial/field_division): remove `polynomial.div` and `polynomial.mod` This leaves us with only one spelling for each, `/` and `%`.
References
eric-wieser/tidy-field_division
Author
eric-wieser
Parents
2c6df07f
Loading