Commit 2021-08-18 08:28 11516119
View on Github →feat(algebra/pointwise): instances in locale pointwise (#8689)
@rwbarton and @bryangingechen mentioned in https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Friday.20afternoon.20puzzle.20--.2037.20.E2.88.88.2037.3F that we should put pointwise instances on sets in a locale.
This PR does that. You now have to write open_locale pointwise to get algebraic operations on sets and finsets.