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