mathlib3

c57cfc6d - feat({data/{finset,set},order/filter}/pointwise): Pointwise monoids are division monoids (#13900)

feat({data/{finset,set},order/filter}/pointwise): Pointwise monoids are division monoids (#13900) `α` is a `division_monoid` implies that `set α`, `finset α`, `filter α` are too. The core result needed for this is that `s` is a unit in `set α`/`finset α`/`filter α` if and only if it is equal to `{u}`/`{u}`/`pure u` for some unit `u : α`.