FLT/Mathlib/Topology/Algebra/Module/CompactOpen.lean

The compact-open topology on continuous linear maps

This file endows M1 →L[k] M2 with the topology induced from the compact-open topology on C(M1, M2), as scoped instances in the ContinuousLinearMap.CompactOpen namespace, and shows that it makes M1 →L[k] M2 a topological k-module.

These instances are scoped since they may differ from the topology of bounded convergence used elsewhere in Mathlib for continuous linear maps between uniform modules.

Material destined for a new file Mathlib.Topology.Algebra.Module.CompactOpen.