n_ary): Binary image of finsets (#13718)

Commit

3 years ago

feat(data/finset/n_ary): Binary image of finsets (#13718) Define `finset.image₂`, the binary map of finsets. Golf `data.finset.pointwise` using it.

Author

YaelDillies

Parents