github project

Stream: condensed mathematics

[Johan Commelin]

https://github.com/leanprover-community/lean-liquid/projects/2 contains some cards that keep track of the main ingredients needed to complete the project.

[Filippo A. E. Nuccio]

I have seen the card on proving that $\mathbb{R}$ is a quotient of $\mathbb{Z}((T))_r$: if you mean the surjection as "normal" spaces, this is done, but may be you meant the whole exactness in thm 6.9?

[Johan Commelin]

@Filippo A. E. Nuccio I'll leave it up to you how you want to interpret it. Feel free to edit or close it.

[Filippo A. E. Nuccio]

Ok (also, I haven't forgotten that I still need to update the blueprint with links to Lean code, but I am a bit obsessed with the exactness of 6.9 these days... :upside_down: )