instHasCokernelInr

Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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