Topology on ZMod N

We equip ZMod N with the discrete topology.

instance ZMod.instTopologicalSpace {N : ℕ} : TopologicalSpace (ZMod N)

The discrete topology (every set is open).

Equations

• ZMod.instTopologicalSpace = ⊥

instance ZMod.instDiscreteTopology {N : ℕ} : DiscreteTopology (ZMod N)

Equations

• ⋯ = ⋯