mathlib3

23892a05 - chore(analysis/normed_space/operator_norm): semilinearize part of the file (#10076)

chore(analysis/normed_space/operator_norm): semilinearize part of the file (#10076) This PR generalizes part of the `operator_norm` file to semilinear maps. Only the first section (`semi_normed`) is done, which allows us to construct continuous semilinear maps using `linear_map.mk_continuous`. The rest of the file is trickier, since we need specify how the ring hom interacts with the norm. I'd rather leave it to a future PR since I don't need the rest now.