Commit 2022-05-12 12:10 c57cfc6d

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