Commit 2021-09-24 21:40 8ff756cb

feat(group_theory/*/pointwise): Copy set lemmas about pointwise actions to subgroups and submonoids (#9359) This is pretty much just a copy-and-paste job. At least the proofs themselves don't need copying. The set lemmas being copied here are: https://github.com/leanprover-community/mathlib/blob/a9cd8c259d59b0bdbe931a6f8e6084f800bd7162/src/algebra/pointwise.lean#L607-L680 I skipped the preimage_smul lemma for now because I couldn't think of a useful statement using map.