instHasInitial — Mathlib

English

Initial object exists in the category of commutative group objects; uniqueness up to isomorphism arises from the trivial structure.

Русский

Начальный объект существует в категории комм-групп, уникальность поизоморфизму следует из тривиальной структуры.

LaTeX

$$$\\text{HasInitial }(\\text{CommGrp}_C)$$$

Lean4

instance : HasInitial (CommGrp_ C) :=
  hasInitial_of_unique (trivial C)

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