Commit 2025-09-18 12:51 b79638e2

refactor(Analysis/Calculus/FDeriv): split off material on composing continuous linear maps (#29753) This PR splits off the first sections of FDeriv/Mul.lean, concerning the applying of continuous linear maps, into a new file. This material is unused in the rest of the file and does not have much to do with multiplication of functions either. Another motivation for this change is that FDeriv/Mul.lean is on the long pole and in the build trace it appears with only one other file being built continuously. By splitting it up and reducing its dependencies, we should be able to improve parallelism. https://speed.lean-lang.org/mathlib4-out/b16bc96c8fa8c9b828fd6b48607becccee06d77f/