instIsGroupoid

Mathlib.CategoryTheory.Groupoid

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instIsGroupoid

English

If C is a groupoid, then C is a category in which every morphism is invertible.

Русский

Если C является группоидом, то это категория, в которой каждая морфизм обратим.

LaTeX

$$$\mathrm{IsGroupoid}(C)$$$

Lean4

noncomputable instance {C : Type u} [Groupoid.{v} C] : IsGroupoid C where

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

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

Разделы

Аффилиация

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