Commit 2021-11-01 10:12 23892a05

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.