basic): generalize `finset.prod_of_empty` (#18045)

Commit

3 years ago

chore(algebra/big_operators/basic): generalize `finset.prod_of_empty` (#18045) This also generalizes `prod_empty` to arbitrary `fintype` instances.

Author

eric-wieser

Parents