finprod): assorted lemmas
#9121

Open

feat(algebra/big_operators/finprod): assorted lemmas #9121

urkud wants to merge 1 commit into master from finprod-lemmas

Snapshot

f3ea6780

urkud added awaiting-review

urkud added please-adopt

jcommelin removed awaiting-review

kim-em added too-late

Reviewers

No reviews

Assignees

No one assigned

Labels

please-adopt too-late

Milestone

No milestone