structuralIsoOfExpr_horizontalComp

Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Monoidal.structuralIsoOfExpr_horizontalComp

Lean4

theorem structuralIsoOfExpr_horizontalComp {f₁ g₁ f₂ g₂ : C} (η : f₁ ⟶ g₁) (η' : f₁ ≅ g₁) (ih_η : η'.hom = η)
    (θ : f₂ ⟶ g₂) (θ' : f₂ ≅ g₂) (ih_θ : θ'.hom = θ) : (η' ⊗ᵢ θ').hom = η ⊗ₘ θ := by simp [ih_η, ih_θ]

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

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

Разделы

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

Аффилиация

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