mathlib3

2bfa7684 - feat(analysis/normed_space/operator_norm): module and norm instances on continuous semilinear maps (#10494)

feat(analysis/normed_space/operator_norm): module and norm instances on continuous semilinear maps (#10494) This PR adds a module and a norm instance on continuous semilinear maps, generalizes most of the results in `operator_norm.lean` to the semilinear case. Many of these results require the ring homomorphism to be isometric, which is expressed via the new typeclass `[ring_hom_isometric σ]`. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>