mathlib

8624f6db - chore(analysis/normed/group/basic): add `nnnorm_sum_le_of_le` (#13795)

chore(analysis/normed/group/basic): add `nnnorm_sum_le_of_le` (#13795) This is to match `norm_sum_le_of_le`. Also tidies up the coercion syntax a little in `pi.semi_normed_group`. The definition is syntactically identical, just with fewer unecessary type annotations.