instAddCommGroupHom

Mathlib.CategoryTheory.Idempotents.Karoubi

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Idempotents.instAddCommGroupHom

Lean4

instance instAddCommGroupHom [Preadditive C] {P Q : Karoubi C} : AddCommGroup (P ⟶ Q)
    where
  zero_add
    f := by
    ext
    apply zero_add
  add_zero
    f := by
    ext
    apply add_zero
  add_assoc f g
    h' := by
    ext
    apply add_assoc
  add_comm f
    g := by
    ext
    apply add_comm
  neg_add_cancel
    f := by
    ext
    apply neg_add_cancel
  zsmul := zsmulRec
  nsmul := nsmulRec

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

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

Разделы

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

Аффилиация

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