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