ZMod n acts continuously on discrete spaces

ZMod n carries the discrete topology, so its scalar action on any discrete space is continuous. This is the topological hypothesis of a discrete module with ZMod n coefficients.

Main results

• TauCeti.ZMod.continuousSMul_of_discreteTopology: ZMod n acts continuously on a discrete space.

instance TauCeti.ZMod.continuousSMul_of_discreteTopology {n : ℕ} {M : Type u_1} [TopologicalSpace M] [DiscreteTopology M] [SMul (ZMod n) M] : ContinuousSMul (ZMod n) M

ZMod n acts continuously on a discrete space, both factors of ZMod n × M being discrete.