Commit 2021-10-27 15:13 a3f4a025
View on Github →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.