mathlib3

4f4a9b58 - feat(analysis/analytic/inverse): inverse of a formal multilinear series (#5852)

feat(analysis/analytic/inverse): inverse of a formal multilinear series (#5852) We construct the left inverse and a right inverse of a formal multilinear series with invertible first term, and we show that they coincide.