mathlib

e9a11f6e - feat(analysis/normed_space/operator_norm): generalize to seminormed space (#7202)

feat(analysis/normed_space/operator_norm): generalize to seminormed space (#7202) This PR is part of a series of PRs to have seminormed stuff in mathlib. We generalize here `operator_norm` to `semi_normed_space`. I didn't do anything complicated, essentially I only generalized what works out of the box, without trying to modify the proofs that don't work.