mathlib
f55e3ce4 - refactor(*): move `algebra` below `polynomial` in the `import` chain (#2294)

Commit
6 years ago
refactor(*): move `algebra` below `polynomial` in the `import` chain (#2294) * Move `algebra` below `polynomial` in the `import` chain This PR only moves code and slightly generalizes `mv_polynomial.aeval`. * Fix compile * Update src/data/mv_polynomial.lean * Apply suggestions from code review * Apply suggestions from code review Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Author
Parents
Loading