Mathlib Changelog
v4
Changelog
About
Github
Theorem
CondensedSet.isDiscrete_tfae
Modification history
2025-03-13 02:38
Mathlib/Condensed/Discrete/Characterization.lean
chore: whitespace again (#22878) …
Modified
CondensedSet.isDiscrete_tfae
View on Github →
2024-10-17 08:31
Mathlib/Condensed/Discrete/Characterization.lean
feat(Condensed): characterisation of discrete (light) condensed sets and modules (#14027) …
Added
CondensedSet.isDiscrete_tfae
View on Github →