instZero

Mathlib.CategoryTheory.Idempotents.Karoubi

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

Lean4

@[simps zero]
instance instZero [Preadditive C] {P Q : Karoubi C} : Zero (P ⟶ Q) where
  zero := ⟨0, by simp only [comp_zero, zero_comp]⟩

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

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

Разделы

Аффилиация

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