Lagrange inversion formula

Stream: Is there code for X?

[Philippe Duchon]

Does Mathlib know about Lagrange's formula for the compositional inverse of a power series? I found the multiplicative inverse, but leansearch does not seem to find anything for the compositional inverse.

Even the very basic case of single-variable, formal power series with rational coefficients is a staple of enumerative combinatorics.

[Sébastien Gouëzel]

We have docs#FormalMultilinearSeries.leftInv_comp and everything in this file.

[Philippe Duchon]

Hmm... I would not have recognized it in this form. Thanks!

[Weiyi Wang]

This constructs the inverse, but is there a theorem shows that the Lagrange inversion formula holds for it?

[Weiyi Wang]

Separately, if we do have it, we should add it here https://github.com/leanprover-community/mathlib4/blob/449fcb10feb34b6a5c8ca9f8917e33015ee249aa/docs/1000.yaml#L539C1-L540

[Sébastien Gouëzel]

We don't have the explicit formula for the coefficients in the Lagrange inversion formula, as far as I can tell.