Commit 2022-01-21 22:19 d99f2fd7
View on Github →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.