Def CompHausLike.LocallyConstantModule.functorToPresheaves

Modification history

2024-10-04 11:14
Mathlib/Condensed/Discrete/Module.lean
feat(Condensed): discrete condensed modules are given by locally constant maps (#15569) …
Added CompHausLike.LocallyConstantModule.functorToPresheavesView on Github →