evalWhiskerRightAux_of

Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

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

Lean4

theorem evalWhiskerRightAux_of {f g : C} (η : f ⟶ g) (h : C) : η ▷ h = (Iso.refl _).hom ≫ η ▷ h ≫ (Iso.refl _).hom := by
  simp

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

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

Разделы

Аффилиация

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