Commit 2020-09-16 11:42 623c8462

View on Github →

feat(data/mv_polynomial/variables): add facts about vars and mul (#4149) More from the Witt vectors branch. Co-authored by: Johan Commelin johan@commelin.net

Estimated changes

Modified src/data/mv_polynomial/variables.lean

added theorem mv_polynomial.vars_C_mul

added theorem mv_polynomial.vars_mul

added theorem mv_polynomial.vars_one

added theorem mv_polynomial.vars_pow

added theorem mv_polynomial.vars_prod