Mathlib v3 is deprecated. Go to Mathlib v4

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 in linear_equiv.continuous_symm;
  • add a few simp lemmas.

Estimated changes