banach): use bundled `→L[𝕜]` maps
#2107

Merged

refactor(analysis/normed_space/banach): use bundled `→L[𝕜]` maps #2107

mergify merged 2 commits into master from banach-bundled

refactor(analysis/normed_space/banach): use bundled `→L[𝕜]` maps

4a9f9a18

jcommelin approved these changes on 2020-03-09

jcommelin added ready-to-merge

Merge branch 'master' into banach-bundled

acc0919d

mergify merged 4258f5ee into master 6 years ago

mergify deleted the banach-bundled branch 6 years ago

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone