# [isabelle] Formal_Power_Series.thy and inversion

`While working my way through GouldBk.pdf with FormaI_Power_Series.thy I
``am at the Lagrange Inversion theorems and I am stuck. At present the
``problem is with:
`
fps_inv g -- when g is delta, i.e. g=0 + a_1*X+a_2*X^2 ...
This is defined as fps=0.0.0...

`Which I don't understand. How is that justified? That change is
``referred to in the 2016 news (more or less). This seems to be a major
``roadblock; alternate interpretations are that the "res" function of
``Laurent series are missing.
``Amine Chaieb referred to a Formal Power Series structure that included
``Laurent Series in 2009 talk, but I can't seem to find the talk or any
``reference in Isabelle . Does anybody have a pointer?
`I can implement Niven's Laurent extension in
https://www.maa.org/sites/default/files/pdf/upload_library/22/Ford/IvanNiven.pdf
but that would delay any interesting work even further (:

`I tried another approach but the prematurely declaring zero and not
``waiting for cancellation possibilities has struck at me again. The
``whole term does have a cancellation if the term is multiplied by X and
``yields fps $0 =1; at least from an outside algebra point of view.
`A particularly simple Lagrange rendering is at:
http://users.math.msu.edu/users/magyar/Math880/Lagrange.pdf
(with a few typos).

`Or I can try the Umbral calculus version but that also seems as hard as
``Niven.
`
Ray
--
From the QED manifesto:https://www.cs.ru.nl/~freek/qed/qed.html
"
Mathematics is arguably the foremost creation of the human mind.
"

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*