Commit 2022-10-06 17:50 5b0dd140
View on Github →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 inanalysis.normed.group.basic
. To disambiguate names, I add one or two'
to the multiplicative version where needed.