comp_proof

Mathlib.CategoryTheory.Idempotents.Karoubi

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

English

Another instance of associativity-based simplification for nested compositions in Karoubi.

Русский

Ещё один случай упрощения по ассоциации для вложенных композиций в Кароуоби.

LaTeX

$$P.p ≫ (f.f ≫ g.f) ≫ R.p = f.f ≫ g.f$$

Lean4

theorem comp_proof {P Q R : Karoubi C} (g : Hom Q R) (f : Hom P Q) : P.p ≫ (f.f ≫ g.f) ≫ R.p = f.f ≫ g.f := by simp

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

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

Разделы

Аффилиация

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