Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-08 09:53 7c070c4d

View on Github →

feat(data/finset/basic): Coercion of a product of finsets (#15011) ↑(∏ i in s, f i) : set α) = ∏ i in s, ↑(f i) for f : ι → finset α.

Estimated changes