image

Mathlib.CategoryTheory.Abelian.Images

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

Lean4

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

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

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

Разделы

Аффилиация

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