eval_tensorHom

Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

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

Lean4

theorem eval_tensorHom {f g h i : C} {η η' : f ⟶ g} {θ θ' : h ⟶ i} {ι : f ⊗ h ⟶ g ⊗ i} (e_η : η = η') (e_θ : θ = θ')
    (e_ι : η' ⊗ₘ θ' = ι) : η ⊗ₘ θ = ι := by simp [e_η, e_θ, e_ι]

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

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

Разделы

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

Аффилиация

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