PR #9121: feat(algebra/big_operators/finprod): assorted l...

Stream: triage

[Random Issue Bot]

Today I chose PR 9121 for discussion!

feat(algebra/big_operators/finprod): assorted lemmas
Created by @Yury G. Kudryashov (@urkud) on 2021-09-09
Labels: please-adopt

Is this PR still relevant? Any recent updates? Anyone making progress?