LiftHom_tensor

Mathlib.Tactic.CategoryTheory.Coherence

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Coherence.LiftHom_tensor

Lean4

instance LiftHom_tensor {W X Y Z : C} [LiftObj W] [LiftObj X] [LiftObj Y] [LiftObj Z] (f : W ⟶ X) (g : Y ⟶ Z)
    [LiftHom f] [LiftHom g] : LiftHom (f ⊗ₘ g) where lift := LiftHom.lift f ⊗ₘ LiftHom.lift g

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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