Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - refactor(data/polynomial): Move some lemmas to monoid_algebra #4627

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - refactor(data/polynomial): Move some lemmas to monoid_algebra #4627

wants to merge 4 commits into from

Commits on Oct 15, 2020

  1. refactor(data/polynomial): Move some lemmas to monoid_algebra 

    The `add_monoid_algebra.mul_apply_antidiagonal` lemma is copied verbatim from `monoid_algebra.mul_apply_antidiagonal`.
    @eric-wieser
    eric-wieser committed Oct 15, 2020
    Configuration menu
    Copy the full SHA
    2dec134 View commit details
    Browse the repository at this point in the history

  2. refactor(data/polynomial): Remove an unnecessary use of coeff_single 

    The docstring for `coeff_single` says it shouldn't be needed and `coeff_monomial` is the preferred spelling
    @eric-wieser
    eric-wieser committed Oct 15, 2020
    Configuration menu
    Copy the full SHA
    d577a63 View commit details
    Browse the repository at this point in the history

  3. refactor(data/polynomial): Golf proofs with existing lemmas 

    This allows the lemma which "ideally wouldn't be necessary" to not be necessary
    @eric-wieser
    eric-wieser committed Oct 15, 2020
    Configuration menu
    Copy the full SHA
    75646cd View commit details
    Browse the repository at this point in the history

  4. Update src/data/polynomial/basic.lean

    @eric-wieser
    eric-wieser committed Oct 15, 2020
    Configuration menu
    Copy the full SHA
    b112b92 View commit details
    Browse the repository at this point in the history