instHasCokernelInl

Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.instHasCokernelInl

English

There exists a cokernel of biprod.inl, i.e., HasCokernel (biprod.inl).

Русский

Существует кокерел biprod.inl, то есть HasCokernel (biprod.inl).

LaTeX

$$$\text{HasCokernel}(\mathrm{biprod.inl})$$$

Lean4

instance : HasCokernel (biprod.inl : X ⟶ X ⊞ Y) :=
  HasColimit.mk ⟨_, biprod.isCokernelInlCokernelFork X Y⟩

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

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

Разделы

Аффилиация

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