Commit 2020-10-15 16:29 46b0528b

View on Github →

refactor(data/polynomial): Move some lemmas to monoid_algebra (#4627) The add_monoid_algebra.mul_apply_antidiagonal lemma is copied verbatim from monoid_algebra.mul_apply_antidiagonal.

Estimated changes

Modified src/algebra/monoid_algebra.lean

added theorem add_monoid_algebra.mul_apply_antidiagonal

Modified src/data/polynomial/algebra_map.lean

Modified src/data/polynomial/basic.lean

modified def polynomial.coeff

deleted theorem polynomial.coeff_single

Modified src/data/polynomial/coeff.lean