Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-02 05:51 f55e3ce4

View on Github →

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

Estimated changes

added theorem mv_polynomial.aeval_C
added theorem mv_polynomial.aeval_X
added def polynomial.aeval
added theorem polynomial.aeval_C
added theorem polynomial.aeval_X
added theorem polynomial.aeval_def
added theorem polynomial.eval_unique
deleted def mv_polynomial.aeval
deleted theorem mv_polynomial.aeval_C
deleted theorem mv_polynomial.aeval_X
deleted theorem mv_polynomial.aeval_def
deleted theorem mv_polynomial.eval_unique
deleted def polynomial.aeval
deleted theorem polynomial.aeval_C
deleted theorem polynomial.aeval_X
deleted theorem polynomial.aeval_def
deleted theorem polynomial.eval_unique