analysis overview

Stream: maths

[Johan Commelin]

Is https://leanprover-community.github.io/mathlib-overview.html#analysis missing the recent advances in complex analysis?

[Moritz Doll]

I think there are quite a lot things that got added recently in analysis that are not in that list (Banach-Steinhaus, bornology, locally convex spaces,..)

[Moritz Doll]

I thought about adding these, but I haven't found the time yet and implementing math is more fun than writing documentation

[Johan Commelin]

I know all to well what you mean