mathlib3

6cadbc0d - feat(analysis/normed/group/pointwise): Multiplicativise (#17023)

feat(analysis/normed/group/pointwise): Multiplicativise (#17023) Write the multiplicative version of all lemmas in `analysis.normed.group.pointwise` and move unrelated lemmas to `analysis.normed.group.basic` (including deleting a duplicate)