feat(algebra/pointwise): add preimage_smul and generalize a couple of assumptions (#8600)
feat(algebra/pointwise): add preimage_smul and generalize a couple of assumptions (#8600)

Some lemmas about smul spun off from #2819 





leanprover-community/mathlib,leanprover-community/mathlib