Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-03 04:08 ab3a26d5

View on Github →

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

Estimated changes

Modified src/algebra/big_operators/basic.lean

modified theorem finset.prod_of_empty

modified theorem fintype.prod_empty

modified theorem fintype.prod_unique