instUnique

Mathlib.Data.ZMod.Defs

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

English

The type ZMod(1) is a singleton (Unique).

Русский

Тип ZMod(1) есть синглтон (уникален).

LaTeX

$$$Unique\ (ZMod(1)).$$$

Lean4

instance instUnique : Unique (ZMod 1) :=
  Fin.instUnique

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

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

Разделы

Аффилиация

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