Commit 2020-05-06 19:39 b1c0398a
View on Github →feat(analysis/analytic/composition): the composition of formal series is associative (#2513) The composition of formal multilinear series is associative. I will need this when doing the analytic local inverse theorem, and I was surprised by how nontrivial this is: one should show that two double sums coincide by reindexing, but the reindexing is combinatorially tricky (it involves joining and splitting lists carefully). Preliminary material on lists, sums and compositions is done in #2501 and #2554, and the proof is in this PR.