Commit 2021-02-07 04:02 4b035fcd

refactor(analysis/normed_space): upgrade linear_map.to_continuous_linear_map to linear_equiv (#6072) This way Lean will simplify, e.g., f.to_continuous_linear_map = 0 to f = 0.