instTopologicalSpace

Mathlib.Topology.Instances.ZMod

URI: https://scilib.ai/kg/mathlib#ZMod.instTopologicalSpace

English

Each ZMod N carries the discrete topology.

Русский

Каждый ZMod N имеет дискретную топологию.

LaTeX

$$$\\text{TopologicalSpace}(\\mathbb{Z}/N\\mathbb{Z})$ is discrete$$

Lean4

/-- The discrete topology (every set is open). -/
instance : TopologicalSpace (ZMod N) :=
  ⊥

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru