normed_space): prove the conformality of `symm` of conformal `linear_equiv` and `local_homeomorph`
#9623

Open

feat(analysis/normed_space/conformal_linear_map, analysis/calculus/conformal/normed_space): prove the conformality of `symm` of conformal `linear_equiv` and `local_homeomorph` #9623

justadzr wants to merge 3 commits into master from conformality-of-inverse

add `symm`

6bae0ef2

add docstrings

4d06d335

justadzr added awaiting-review

fix grammar

68485e81

hrmacbeth commented on 2021-10-09

hrmacbeth removed awaiting-review

hrmacbeth added awaiting-author

leanprover-community-bot-assistant added merge-conflict

kim-em added too-late

Reviewers

hrmacbeth

Assignees

No one assigned

Labels

awaiting-author merge-conflict too-late

Milestone

No milestone