instBialgebraCarrierUnopCommAlgCatOfMonObjOpposite

Mathlib.Algebra.Category.CommBialgCat

URI: https://scilib.ai/kg/mathlib#instBialgebraCarrierUnopCommAlgCatOfMonObjOpposite

Lean4

instance (A : (CommAlgCat R)ᵒᵖ) [MonObj A] : Bialgebra R A.unop :=
  .ofAlgHom μ[A].unop.hom η[A].unop.hom congr(($((MonObj.mul_assoc_flip A).symm)).unop.hom)
    congr(($(MonObj.one_mul A)).unop.hom) congr(($(MonObj.mul_one A)).unop.hom)

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

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

Разделы

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

Аффилиация

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