Theorem continuous_linear_map.exists_mul_lt_of_lt_op_norm

refactor(analysis): change the symbol for norm to align with the unicode spec (#17575) …

feat(analysis/normed_space/operator_norm): characterize the operator norm over a `densely_normed_field` in terms of the supremum (#16963) …