Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-01 05:20 31ba155f

View on Github →

feat(algebraic_topology/cech_nerve): The Cech nerve is a right adjoint. (#7716) Also fixes the namespace in the file algebraic_topology/cech_nerve.lean. This is needed for LTE

Estimated changes