subsingleton_units

Mathlib.Data.ZMod.Basic

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

English

In ZMod 2, the group of units is singleton.

Русский

В ZMod 2 группа единиц тривиальна.

LaTeX

$$Subsingleton (Units (ZMod 2))$$

Lean4

instance subsingleton_units : Subsingleton (ZMod 2)ˣ :=
  ⟨by decide⟩

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

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

Разделы

Аффилиация

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