whiskerLeft_hom

Mathlib.CategoryTheory.Monoidal.Grp_

URI: https://scilib.ai/kg/mathlib#Grp_.whiskerLeft_hom

Lean4

@[simp]
theorem whiskerLeft_hom {G H : Grp_ C} (f : G ⟶ H) (I : Grp_ C) : (f ▷ I).hom = f.hom ▷ I.X :=
  rfl

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

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

Разделы

Аффилиация

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