cokernelOpOp

Mathlib.CategoryTheory.Abelian.Opposite

URI: https://scilib.ai/kg/mathlib#CategoryTheory.cokernelOpOp

← MathLib Explorer

English

For f,g,h, (f − g) ≫ h = f ≫ h − g ≫ h.

Русский

Для f,g,h выполняется (f − g) ≫ h = f ≫ h − g ≫ h.

LaTeX

$$$ (f - g) \circ h = f \circ h - g \circ h $$$

Lean4

/-- The cokernel of `f.op` is the opposite of `kernel f`. -/
@[simps!]
def cokernelOpOp : cokernel f.op ≅ Opposite.op (kernel f) :=
  (cokernelOpUnop f).op.symm

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

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

Разделы

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

Аффилиация

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