Commit 2025-12-11 11:46 c8f4d329

View on Github →

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

Estimated changes

Modified Mathlib/Topology/Algebra/Module/StrongTopology.lean

added def ContinuousLinearMap.postcomp_compactConvergenceCLM

added def ContinuousLinearMap.precomp_compactConvergenceCLM