Zulip Chat Archive

Stream: condensed mathematics

Topic: github project


Johan Commelin (Nov 29 2021 at 12:58):

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 (Nov 30 2021 at 14:46):

I have seen the card on proving that R\mathbb{R} is a quotient of Z((T))r\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 (Nov 30 2021 at 14:56):

@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 (Nov 30 2021 at 14:57):

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: )


Last updated: Dec 20 2023 at 11:08 UTC