groupoid

Mathlib.CategoryTheory.Quotient

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Quotient.groupoid

Lean4

/-- The quotient of a groupoid is a groupoid. -/
instance groupoid : Groupoid (Quotient r) where
  inv f := Quotient.inv r f
  inv_comp f := Quot.inductionOn f <| by simp [CategoryStruct.comp, CategoryStruct.id]
  comp_inv f := Quot.inductionOn f <| by simp [CategoryStruct.comp, CategoryStruct.id]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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