mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(algebra/big_operators/finprod): assorted lemmas

Open urkud opened this issue 3 years ago • 1 comments

These lemmas come from an old version of #8903. I don't need them anymore, so feel free to reject or drop some of the lemmas before merging.

Open in Gitpod

urkud avatar Sep 09 '21 20:09 urkud

Until someone picks this up, I will remove the awaiting-review label. I don't think this needs much improvement; but otoh, it's not clear that we need this statements. So until the need is there, I don't think we should merge this. Agreed?

jcommelin avatar Sep 30 '21 06:09 jcommelin