mathlib3

1843bfc9 - feat(algebra/pointwise): pointwise scalar-multiplication lemmas (#1925)

feat(algebra/pointwise): pointwise scalar-multiplication lemmas (#1925) * feat(algebra/pointwise): more lemmas about scaling sets - rename `smul_set` to `scale_set` for disambiguation - define `scale_set_action`, which subsumes `one_smul_set` - additional lemmas lemmas * fix(analysis/convex): refactor proofs for `scale_set` * feat(algebra/pointwise): re-organise file - subsume `pointwise_mul_action` * feat(algebra/pointwise): remove `pointwise_mul_action` - subsumed by `smul_set_action` with left-regular action. Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>