mathlib3
1ca33274 - Merge branch 'master' into erd1/finsupp_lemmas

Commit

2 years ago

Merge branch 'master' into erd1/finsupp_lemmas

References

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

Author

eric-wieser

eric-wieser

Parents

Loading