Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(data/finset/noncomm_prod): add noncomm_prod_mul_distrib #12524

Closed
wants to merge 9 commits into from
Closed

[Merged by Bors] - feat(data/finset/noncomm_prod): add noncomm_prod_mul_distrib #12524

wants to merge 9 commits into from

Commits on Mar 8, 2022

  1. feat(data/finset/noncomm_prod): add noncomm_prod_commute 

    adding `list.prod_commute`, `multiset.noncomm_prod_commute` and
`finset.noncomm_prod_commute`.
    @nomeata
    nomeata committed Mar 8, 2022
    Configuration menu
    Copy the full SHA
    e5668d5 View commit details
    Browse the repository at this point in the history

  2. feat(data/finset/noncomm_prod): add noncomm_prod_mul_distrib 

    The non-commutative version of `finset.sum_union`
    @nomeata
    nomeata committed Mar 8, 2022
    Configuration menu
    Copy the full SHA
    b8ce57f View commit details
    Browse the repository at this point in the history

  3. Update src/data/list/prod_monoid.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @nomeata @eric-wieser
    nomeata and eric-wieser committed Mar 8, 2022
    Configuration menu
    Copy the full SHA
    711bb2f View commit details
    Browse the repository at this point in the history

  4. Merge branch 'joachim/noncomm_prod_commute' into joachim/noncomm_prod… 

    …_mul_distrib
    @nomeata
    nomeata committed Mar 8, 2022
    Configuration menu
    Copy the full SHA
    de2c154 View commit details
    Browse the repository at this point in the history

  5. Merge commit '4ad5c5a33891424f0807c4dc9aaa222deb6ce522' into joachim/… 

    …noncomm_prod_commute
    @nomeata
    nomeata committed Mar 8, 2022
    Configuration menu
    Copy the full SHA
    2c65097 View commit details
    Browse the repository at this point in the history

  6. Merge branch 'joachim/noncomm_prod_commute' into joachim/noncomm_prod… 

    …_mul_distrib
    @nomeata
    nomeata committed Mar 8, 2022
    Configuration menu
    Copy the full SHA
    6c9217c View commit details
    Browse the repository at this point in the history

  7. Fix proof

    @nomeata
    nomeata committed Mar 8, 2022
    Configuration menu
    Copy the full SHA
    7041eb9 View commit details
    Browse the repository at this point in the history

Commits on Mar 9, 2022

  1. Update src/data/finset/noncomm_prod.lean

    @nomeata
    nomeata committed Mar 9, 2022
    Configuration menu
    Copy the full SHA
    b06785c View commit details
    Browse the repository at this point in the history

Commits on Mar 11, 2022

  1. Pull proof from lemma statement into separate lemma

    @nomeata
    nomeata committed Mar 11, 2022
    Configuration menu
    Copy the full SHA
    98e83b8 View commit details
    Browse the repository at this point in the history