Commit 2023-07-06 13:05 8905e5ed

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 and 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:.