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 α
.
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 α
.