mv_polynomial): doc comments and removing unused arguments
#1585

Merged

chore(src/data/mv_polynomial): doc comments and removing unused arguments #1585

mergify merged 3 commits into master from mv_polynomial_lint

chore(src/data/mv_polynomial): doc comments and removing unused argum…

af098105

kim-em commented on 2019-10-22

Update src/data/mv_polynomial.lean

430c7f52

jcommelin commented on 2019-10-22

robertylewis approved these changes on 2019-10-23

robertylewis added ready-to-merge

Merge branch 'master' into mv_polynomial_lint

5655cfb0

mergify merged 24dd80b0 into master 6 years ago

mergify deleted the mv_polynomial_lint branch 6 years ago

Reviewers

robertylewis

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone