Commit 2024-06-07 09:26 678f4912

View on Github →

feat(Condensed): explicit sheaf condition for light condensed sets (#13503)

depends on: #13501

Estimated changes

Modified Mathlib.lean

Created Mathlib/Condensed/Light/Explicit.lean

added theorem LightCondensed.equalizerCondition