mathlib

8ff756cb - feat(group_theory/*/pointwise): Copy set lemmas about pointwise actions to subgroups and submonoids (#9359)

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`.