Commit 2021-12-03 17:46 92fafba2

View on Github →

feat(data/(mv_)polynomial): add aeval_prod and aeval_sum for (mv_)polynomial (#10594) Another couple of small polynomial helper lemmas from flt-regular.

Estimated changes

Modified src/data/mv_polynomial/basic.lean

added theorem mv_polynomial.aeval_prod

added theorem mv_polynomial.aeval_sum

Modified src/data/polynomial/algebra_map.lean

added theorem polynomial.aeval_prod

added theorem polynomial.aeval_sum