coimage

Mathlib.CategoryTheory.Abelian.Images

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Abelian.coimage

Lean4

/-- The cokernel of the kernel of `f` is called the (abelian) coimage of `f`. -/
protected abbrev coimage : C :=
  cokernel (kernel.ι f)

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

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

Разделы

Аффилиация

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