mathlib

8905e5ed - feat(topology/algebra/module/strong_topology): golf `arrow_congrSL` introduced in #19107 (#19128)

feat(topology/algebra/module/strong_topology): golf `arrow_congrSL` introduced in #19107 (#19128) I added more general definitions `precomp` and `postcomp` for expressing that (pre/post)-composing by a *fixed* continuous linear maps is continuous. These were planned about a year ago when I defined the strong topology and follow from [uniform_on_fun.precomp_uniform_continuous](https://leanprover-community.github.io/mathlib_docs/topology/uniform_space/uniform_convergence_topology.html#uniform_on_fun.precomp_uniform_continuous) and [uniform_on_fun.postcomp_uniform_continuous](https://leanprover-community.github.io/mathlib_docs/topology/uniform_space/uniform_convergence_topology.html#uniform_on_fun.postcomp_uniform_continuous). The proof of continuity of `arrow_congrSL` is a direct consequence of these, so we don't have to do it by hand. This is not really a "golf" since I added more lines than I removed, but these more general constructions will be needed at some point anyway (my use case was distribution theory) so I'm doing some proactive golfing :smile:.