Commit 2019-10-23 12:50 24dd80b0
View on Github →chore(src/data/mv_polynomial): doc comments and removing unused arguments (#1585)
- chore(src/data/mv_polynomial): doc comments and removing unused arguments
- Update src/data/mv_polynomial.lean
chore(src/data/mv_polynomial): doc comments and removing unused arguments (#1585)