coreCategory_comp_iso

Mathlib.CategoryTheory.Core

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

Lean4

@[simp]
theorem coreCategory_comp_iso {x y z : Core C} (f : x ⟶ y) (g : y ⟶ z) : (f ≫ g).iso = f.iso ≪≫ g.iso :=
  rfl

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

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

Разделы

Аффилиация

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