Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-08-01 20:50
e318dc80
View on Github →
refactor(Condensed): merge files about discreteness (
#15402
)
Estimated changes
Modified
Mathlib.lean
Deleted
Mathlib/Condensed/Discrete.lean
Created
Mathlib/Condensed/Discrete/Basic.lean
Deleted
Mathlib/Condensed/Light/Discrete.lean