feat: specialize [pre, post]comp_uniformConvergenceCLM to CompactConvergenceCLM (leanprover-community#32395)

Author: ADedecker

Mathlib/Topology/Algebra/Module/StrongTopology.lean

@@ -560,8 +560,7 @@ def postcomp_uniformConvergenceCLM [IsTopologicalAddGroup F] [IsTopologicalAddGr
       (UniformOnFun.postcomp_uniformContinuous L.uniformContinuous).continuous.comp
         (UniformConvergenceCLM.isEmbedding_coeFn _ _ _).continuous
 
-variable (E)
-
+variable (E) in
 /-- Post-composition by a *fixed* continuous linear map as a continuous linear map.
 
 Note that in non-normed space it is not always true that composition is continuous
@@ -572,7 +571,7 @@ def postcomp [IsTopologicalAddGroup F] [IsTopologicalAddGroup G] [ContinuousCons
   toFun f := L.comp f
   __ := postcomp_uniformConvergenceCLM { S | IsVonNBounded 𝕜₁ S } L
 
-variable (σ F) {E} in
+variable (σ F) in
 lemma toUniformConvergenceCLM_continuous [IsTopologicalAddGroup F]
     [ContinuousConstSMul 𝕜₂ F]
     (𝔖 : Set (Set E)) (h : 𝔖 ⊆ {S | IsVonNBounded 𝕜₁ S}) :
@@ -810,8 +809,11 @@ section CompactSets
 
 /-! ### Topology of compact convergence for continuous linear maps -/
 
-variable {𝕜₁ 𝕜₂ : Type*} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂}
-  {E F : Type*} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F]
+variable {𝕜₁ 𝕜₂ 𝕜₃ : Type*} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂}
+  {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] {E F G : Type*}
+  [AddCommGroup E] [Module 𝕜₁ E]
+  [AddCommGroup F] [Module 𝕜₂ F]
+  [AddCommGroup G] [Module 𝕜₃ G]
 
 variable (E F σ) in
 /-- The topology of compact convergence on `E →L[𝕜] F`. -/
@@ -861,4 +863,29 @@ protected theorem hasBasis_nhds_zero [TopologicalSpace E] [TopologicalSpace F]
 
 end CompactConvergenceCLM
 
+section comp
+
+variable [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G]
+
+open scoped CompactConvergenceCLM
+
+variable (G) in
+/-- Specialization of `ContinuousLinearMap.precomp_uniformConvergenceCLM` to compact
+convergence. -/
+@[simps! apply]
+def ContinuousLinearMap.precomp_compactConvergenceCLM [IsTopologicalAddGroup G]
+    [ContinuousConstSMul 𝕜₃ G] (L : E →SL[σ] F) : (F →SL_c[τ] G) →L[𝕜₃] E →SL_c[ρ] G :=
+  L.precomp_uniformConvergenceCLM G _ _ (fun _ hs ↦ hs.image L.continuous)
+
+variable (E) in
+/-- Specialization of `ContinuousLinearMap.postcomp_uniformConvergenceCLM` to compact
+convergence. -/
+@[simps! apply]
+def ContinuousLinearMap.postcomp_compactConvergenceCLM [IsTopologicalAddGroup F]
+    [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₂ F]
+    (L : F →SL[τ] G) : (E →SL_c[σ] F) →SL[τ] E →SL_c[ρ] G :=
+  L.postcomp_uniformConvergenceCLM _
+
+end comp
+
 end CompactSets