Zulip Chat Archive
Stream: triage
Topic: PR !4#9146: feat(Data/ZMod/Defs): Topological structure o...
Random Issue Bot (Jul 24 2024 at 14:09):
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 (Jul 24 2024 at 14:14):
The titular instance now exists as docs#ZMod.instTopologicalSpace but there are other things in the PR
Last updated: May 02 2025 at 03:31 UTC