Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes