evalHorizontalCompAux_of

Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

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

Lean4

theorem evalHorizontalCompAux_of {f g h i : C} (η : f ⟶ g) (θ : h ⟶ i) :
    η ⊗ₘ θ = (Iso.refl _).hom ≫ (η ⊗ₘ θ) ≫ (Iso.refl _).hom := by simp

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

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

Разделы

Аффилиация

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