Commit 2023-08-09 19:01 a2c34345
View on Github →feat(Topology/ExtremallyDisconnected): prove Gleason's theorem (#5634) This work was done during the 2023 Copenhagen masterclass on formalisation of condensed mathematics. Numerous participants contributed.