Questions about the generating function of Catalan numbers.

Stream: mathlib4

[Brisal]

Hello everyone — I am a graduate student just starting to learn Lean 4. Recently I’ve been browsing some theorems in mathlib and found that there doesn’t seem to be much about generating functions. For example, there doesn’t appear to be a generating function for the Catalan numbers. If I want to formalize the generating function for the Catalan numbers, how should I go about it?

[Yuyang Zhao]

Previously, the API for docs#PowerSeries was not well developed, but it has been much improved now. It might be easier to obtain $\sqrt{1-4x}$ using Hensel's lemma.

[Brisal]

Yuyang Zhao said:

Previously, the API for docs#PowerSeries was not well developed, but it has been much improved now. It might be easier to obtain $\sqrt{1-4x}$ using Hensel's lemma.

ok, I'll try to prove it.