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

Commit

6 years ago

refactor(analysis/normed_space/banach): use bundled `→L[𝕜]` maps (#2107) Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

References

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

Author

urkud

Parents

434b6299

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

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