basic): Coercion of a product of finsets (#15011)

Commit

3 years ago

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

Author

YaelDillies

Parents