feat(algebra/pointwise): Scalar multiplication lemmas (#11486)
This proves a bunch of lemmas about pointwise scalar multiplication of sets, moves `has_vsub` to `algebra.group.defs` and pointwise `vsub` lemmas to `algebra.pointwise`.
I'm also adding a few sections because having `{s t : set α}` is nice for multiplication but not for scalar multiplication.
