Theorem LightCondMod.isDiscrete_tfae

Modification history

2025-03-13 02:38
Mathlib/Condensed/Discrete/Characterization.lean
chore: whitespace again (#22878) …
Modified LightCondMod.isDiscrete_tfaeView on Github →
2024-10-17 08:31
Mathlib/Condensed/Discrete/Characterization.lean
feat(Condensed): characterisation of discrete (light) condensed sets and modules (#14027) …
Added LightCondMod.isDiscrete_tfaeView on Github →