PR !4#9146: feat(Data/ZMod/Defs): Topological structure o...

Stream: triage

[Random Issue Bot]

Today I chose PR 9146 for discussion!

feat(Data/ZMod/Defs): Topological structure on ZMod
Created by @None (@laughinggas) on 2023-12-19
Labels: awaiting-author, merge-conflict, t-topology, t-algebra

Is this PR still relevant? Any recent updates? Anyone making progress?

[Yaël Dillies]

The titular instance now exists as docs#ZMod.instTopologicalSpace but there are other things in the PR