mathlib

d99f2fd7 - chore(analysis/normed/group/basic): merge `norm` and `semi_norm` lemmas on `prod` and `pi` (#11492)

chore(analysis/normed/group/basic): merge `norm` and `semi_norm` lemmas on `prod` and `pi` (#11492) `norm` and `semi_norm` are the same operator, so there is no need to have two sets of lemmas. As a result the elaborator needs a few hints for some applications of the `pi` lemmas, but this is par for the course for pi typeclass instances anyway.