mathlib3

a3f4a025 - chore(analysis/normed_space/is_R_or_C + data/complex/is_R_or_C): make some proof steps standalone lemmas (#9933)

chore(analysis/normed_space/is_R_or_C + data/complex/is_R_or_C): make some proof steps standalone lemmas (#9933) Separate some proof steps from `linear_map.bound_of_sphere_bound` as standalone lemmas to golf them a little bit. Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>