Project status

Stream: condensed mathematics

[Riccardo Brasca]

Dear all, I took a quite long summer break, and I am a little lost about who is doing what. I have time this term to for the LTE, so is there any reasonable project I can work on? Thank's! :big_smile:

[Johan Commelin]

I need to work on teaching stuff. I hope to get back to this question asap.

[Johan Commelin]

But others should feel free to chime in (-;

[Johan Commelin]

@Riccardo Brasca do you want to attempt a mathlib bump in the meantime?

[Riccardo Brasca]

Why not! I am doing it

[Riccardo Brasca]

mathlib bumped

[Adam Topaz]

I've started working on showing that CompHausFiltPseuNormGroup\_1 has limits.

In general, I think we are now working toward getting all the correct definitions in place in order to be able to state the main theorem of the challenge.