comp_p

Mathlib.CategoryTheory.Idempotents.Karoubi

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

English

Same as comp_p, indicating interaction of f with Q.p on the right.

Русский

То же, что и comp_p, отражающее взаимодействие f с Q.p справа.

LaTeX

$$f.f ≫ Q.p = f.f$$

Lean4

@[reassoc (attr := simp)]
theorem comp_p {P Q : Karoubi C} (f : Hom P Q) : f.f ≫ Q.p = f.f := by rw [← f.comm, assoc, assoc, Q.idem]

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

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

Разделы

Аффилиация

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