braiding'_eq_braiding

Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.biprod.braiding'_eq_braiding

English

Equality of braiding isomorphism with its variant: biprod.braiding' P Q = biprod.braiding P Q.

Русский

Равенство изоморфизмов тяги: biprod.braiding' P Q = biprod.braiding P Q.

LaTeX

$$$\mathrm{biprod.braiding'} \ P \ Q = \mathrm{biprod.braiding} \ P \ Q$$$

Lean4

theorem braiding'_eq_braiding {P Q : C} : biprod.braiding' P Q = biprod.braiding P Q := by cat_disch

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

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

Разделы

Аффилиация

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