PR #2259 feat(algebra/big_operators): missing lemmas

feat(algebra/big_operators): missing lemmas #2259

mergify merged 2 commits into master from bigop

feat(algebra/big_operators): missing lemmas

9ae70d3c

jcommelin commented on 2020-03-27

cipher1024 assigned

jcommelin 5 years ago

jcommelin approved these changes on 2020-03-28

jcommelin added ready-to-merge

Merge branch 'master' into bigop

92458f4f

mergify merged d500210b into master 5 years ago

bryangingechen deleted the bigop branch 5 years ago

Reviewers

jcommelin

kim-em

Assignees

jcommelin

Labels

ready-to-merge

Milestone

No milestone