(Un)availability

Stream: general

[Yury G. Kudryashov]

I'm going to grade a large exam for the next 5-7 days. If you want me to do something before it's done, then please @ mention me or write a private message.

[Johan Commelin]

Good luck!

[Yaël Dillies]

Oh @Yury G. Kudryashov could you please have a look at #10676 to see whether I followed your suggestion right?

[Yury G. Kudryashov]

1 more missing @[simp], otherwise LGTM

[Yury G. Kudryashov]

UPD: deadline is after New Year, so I'll mix grading with other activities. Anyway, feel free to tag/PM me if I you want me to do something soon. I know how to say "no".

[Kevin Buzzard]

Please please please work on #10000 :D Impressive-sounding goals like the Riemann zeta function and modular forms are not too far behind!

[Jireh Loreaux]

I'll second Kevin's request. (or at least, if #10000 is pretty stable I'll start basing other things off of it: Liouville's theorem, Gelfand's formula, nonempty spectrum in complex Banach algebras, etc.)

[Yury G. Kudryashov]

I've broken this branch a few minutes ago (merged a new version of #10788). I'll fix it tonight.

[Yury G. Kudryashov]

Anyway, you can consider the main results in integral/complex to be stable (though possibly I'll move it to analysis/)

[Yury G. Kudryashov]

I'll update some lemmas in circle_integral

[Kevin Buzzard]

Thank you so much Yury. For years I've been moaning that we're way behind in real and complex analysis, but now the fact that concrete projects such as modular forms are able to move forwards is an indication that we're finally getting there.

[Yury G. Kudryashov]

One more possible project: prove that a function on $\mathbb C^n$ that has all partial derivatives in metric.closed_ball c r is analytic on the corresponding open ball.

[Yury G. Kudryashov]

The proof is pretty simple (though one should define integral over the product of circles $dz_1dz_2\dots dz_n$).