search

fpvandoorn / lean2

Lean theorem prover version 0.2 (it supports standard and HoTT modes)
Apache License 2.0
0 stars 0 forks source link

formalize cup product for EM-spaces #9

Open fpvandoorn opened 6 years ago

fpvandoorn commented 6 years ago

and afterwards for cohomology

A start is here: https://github.com/cmu-phil/Spectral/blob/master/homotopy/EMRing.hlean