basic): Lemmas regarding `finsupp.filter`
#17012

Open

feat(data/finsupp/basic): Lemmas regarding `finsupp.filter` #17012

erdOne wants to merge 7 commits into master from erd1/finsupp_lemmas

first commit

bbc64ab4

erdOne added awaiting-review

eric-wieser commented on 2022-10-16

rename lemma

33b7a70f

Update basic.lean

144114a7

fix

4ab29eb9

Merge branch 'erd1/finsupp_lemmas' of https://github.com/leanprover-c…

753bd87b

eric-wieser requested a review from

eric-wieser 3 years ago

Vierkantor assigned

Vierkantor 3 years ago

Vierkantor approved these changes on 2022-12-22

leanprover-community-bot-assistant added ready-to-merge

leanprover-community-bot-assistant removed awaiting-review

github-actions added delegated

Merge branch 'master' into erd1/finsupp_lemmas

1ca33274

fix

81cc2824

eric-wieser removed ready-to-merge

eric-wieser added modifies-synchronized-file

kim-em added too-late

kim-em removed delegated

kim-em removed too-late

kim-em added awaiting-review

kim-em added not-too-late

kim-em removed not-too-late

kim-em added too-late

Reviewers

Vierkantor

eric-wieser

Assignees

Vierkantor

Labels

awaiting-review modifies-synchronized-file too-late

Milestone

No milestone