Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-24 22:52 c4760b97

View on Github →

feat(algebra/big_operators/basic): prod/sum over an empty type (#9939)

Estimated changes