Tag Archives: canonical

Prove a theorem. Write a function.

Posted on December 7, 2019 by xenaproject

New maths PhD students Lambert A’Campo and Ashvni Narayanan have proved that a normed real vector space with compact unit ball is finite-dimensional in Lean! [update added a few days later: ROFL Sébastien Gouëzel on the Lean chat complained that … Continue reading →

Posted in General, Imperial, Learning Lean | Tagged Ashvni Narayanan, canonical, collection, compact unit ball, etale cohomology, Grothendieck topology, london school of geometry and number theory, LSGNT, Peter Scholze | 6 Comments

Equality part 3: canonical isomorphism.

Posted on June 2, 2019 by xenaproject

I hadn’t planned on writing a third equality post, but my talk at Big Proof 2019 (see slides here) ended up having a huge section about “mathematician’s equality”, and I realised I had more to say about it. Here are … Continue reading →

Posted in Uncategorized | Tagged canonical, equality | 14 Comments

Tag Archives: canonical

Prove a theorem. Write a function.

Equality part 3: canonical isomorphism.

Categories

Recent Posts