Commit 2025-11-24 04:42 777d704f

View on Github →

feat(Topology/Algebra): generalize precomp and postcomp to UniformConvergenceCLM (#31760)

Estimated changes

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

added def ContinuousLinearMap.postcomp_uniformConvergenceCLM

added def ContinuousLinearMap.precomp_uniformConvergenceCLM