comp

Mathlib.CategoryTheory.Shift.CommShift

URI: https://scilib.ai/kg/mathlib#CategoryTheory.NatTrans.CommShift.comp

English

Instance: NatTrans.CommShift τ A and NatTrans.CommShift τ′ A imply NatTrans.CommShift (τ ≫ τ′) A.

Русский

Инстанс: наличие NatTrans.CommShift τ A и NatTrans.CommShift τ′ A значит NatTrans.CommShift (τ ≫ τ′) A.

LaTeX

$$$NatTrans.CommShift (τ ≫ τ') A$$$

Lean4

instance comp [NatTrans.CommShift τ A] [NatTrans.CommShift τ' A] : NatTrans.CommShift (τ ≫ τ') A where

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

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

Разделы

Аффилиация

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