Commit 2020-05-08 16:39 fc8c4b9f
View on Github →chore(analysis/normed_space/banach
): minor review (#2631)
- move comment to module docstring;
- don't import
bounded_linear_maps
; - reuse
open_mapping
inlinear_equiv.continuous_symm
; - add a few
simp
lemmas.