mathlib3

a49ee49b - feat(data/finset/functor): Functor structures for `finset` (#10980)

feat(data/finset/functor): Functor structures for `finset` (#10980) This defines the monad, the commutative applicative and the (almost) traversable functor structures on `finset`. It all goes in a new file `data.finset.functor` and picks up the `functor` instance that was stranded in `data.finset.basic` by Scott in #2997.