instHasZeroObject

Mathlib.Algebra.Category.Grp.Zero

URI: https://scilib.ai/kg/mathlib#GrpCat.instHasZeroObject

English

The category GrpCat has a zero object, namely the one-element group (PUnit).

Русский

Категория GrpCat имеет нулевой объект, который есть у одной элементной группы (PUnit).

LaTeX

$$$\text{HasZeroObject GrpCat}$ with zero object given by $\mathrm{of}(PUnit)$$$

Lean4

@[to_additive AddGrpCat.hasZeroObject]
instance : HasZeroObject GrpCat :=
  ⟨⟨of PUnit, isZero_of_subsingleton _⟩⟩

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

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

Разделы

Аффилиация

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