mathlib

5b0dd140 - feat(analysis/normed/group/basic): Multiplicative, noncommutative normed groups (#15705)

feat(analysis/normed/group/basic): Multiplicative, noncommutative normed groups (#15705) Define * `seminormed_group` * `seminormed_add_group` * `seminormed_comm_group` * `normed_group` * `normed_add_group` * `normed_comm_group` Multiplicativize all lemmas in `analysis.normed.group.basic`. To disambiguate names, I add one or two `'` to the multiplicative version where needed.