Prequotient

Mathlib.Algebra.Category.MonCat.Colimits

URI: https://scilib.ai/kg/mathlib#MonCat.Colimits.Prequotient

Lean4

/-- An inductive type representing all monoid expressions (without relations)
on a collection of types indexed by the objects of `J`.
-/
inductive Prequotient
  | of : ∀ (j : J) (_ : F.obj j), Prequotient
  | one : Prequotient
  | mul : Prequotient → Prequotient → Prequotient

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

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

Разделы

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

Аффилиация

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