mathlib
b0ece6fe - chore(data/set/{basic,countable}): add, rename, golf (#6935)

Commit
4 years ago
chore(data/set/{basic,countable}): add, rename, golf (#6935) * add `set.range_prod_map` and `set.countable.image2`; * rename `set.countable_prod` to `set.countable.prod`.
Author
Parents
Loading