mathlib3

990a5bbd - chore(analysis/normed_space/extend): remove unnecessary imports (#6538)

chore(analysis/normed_space/extend): remove unnecessary imports (#6538) Remove two imports. `import analysis.complex.basic` is actually unnecessary, `import analysis.normed_space.operator_norm` is indirectly imported via `data.complex.is_R_or_C`.