mathlib

fc8c4b9f - chore(`analysis/normed_space/banach`): minor review (#2631)

chore(`analysis/normed_space/banach`): minor review (#2631) * move comment to module docstring; * don't import `bounded_linear_maps`; * reuse `open_mapping` in `linear_equiv.continuous_symm`; * add a few `simp` lemmas.