mathlib3
4b035fcd - refactor(analysis/normed_space): upgrade `linear_map.to_continuous_linear_map` to `linear_equiv` (#6072)

Commit

4 years ago

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`.

Author

urkud

Parents

736929e5

mathlib3 4b035fcd - refactor(analysis/normed_space): upgrade `linear_map.to_continuous_linear_map` to `linear_equiv` (#6072)

mathlib3
4b035fcd - refactor(analysis/normed_space): upgrade `linear_map.to_continuous_linear_map` to `linear_equiv` (#6072)