Def CompHausLike.LocallyConstant.unit

Modification history

2025-03-12 08:26

Mathlib/Condensed/Discrete/LocallyConstant.lean

chore(whitespace): more changes (#22853) …

Modified CompHausLike.LocallyConstant.unit View on Github →

2024-09-24 05:56

Mathlib/Condensed/Discrete/LocallyConstant.lean

feat(Condensed): discrete condensed sets are given by locally constant maps (#15321) …

Added CompHausLike.LocallyConstant.unit View on Github →