Commit 2021-12-24 03:30 f846a426

feat(algebra/pointwise): expand API for multiplication / addition of finsets by copying the corresponding API for sets (#10600) From flt-regular, I wanted to be able to add finsets so we add a lot of API to show that the existing definition has good algebraic properties by copying the existing set API. Where possible I tried to give proofs that use the existing set lemmas and cast the finsets to sets to make it clear that these are essentially the same lemmas. It would be nice to have a better system for duplicating this API of course, some general versions for set_like or Galois insertions perhaps to unify the theories, but I don't know what that would look like.