mathlib

335232c7 - feat(analysis/normed): `mul_opposite X` inherits the same norm as `X`. (#18470)

feat(analysis/normed): `mul_opposite X` inherits the same norm as `X`. (#18470) This adds a `normed_*` instance for `mul_opposite` everywhere that we also have one for `prod` and `pi`. The intention is to only do this for the additive case. It's not clear to me whether it's sensible to put the same norm on _multiplicative_ normed groups.