mathlib3
feat(analysis/normed_space/multilinear): partially generalize to `semi_normed_group`
#13566
Open
Open