Commit 2023-08-22 17:26 093597d4

View on Github →

feat: projectivity of Stonean in CompHaus (#5808)

  • depends on: #5634
  • depends on: #5761
    This work was done during the 2023 Copenhagen masterclass on formalisation of condensed mathematics. Numerous participants contributed.

Estimated changes

added theorem CompHaus.Gleason
added def CompHaus.lift
added theorem CompHaus.lift_lifts