instBimonObjXXMon

Mathlib.CategoryTheory.Monoidal.Bimon_

URI: https://scilib.ai/kg/mathlib#Bimon.instBimonObjXXMon

Lean4

instance (M : Bimon C) : BimonObj M.X.X where
  counit := ε[M.X].hom
  comul := Δ[M.X].hom
  counit_comul := by rw [← BimonObjAux_counit, ← BimonObjAux_comul, ComonObj.counit_comul]
  comul_counit := by rw [← BimonObjAux_counit, ← BimonObjAux_comul, ComonObj.comul_counit]
  comul_assoc := by simp_rw [← BimonObjAux_comul, ComonObj.comul_assoc]

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

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

Разделы

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

Аффилиация

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