Theorem CategoryTheory.Comonad.left_counit

Modification history

2024-07-20 03:37
Mathlib/CategoryTheory/Monad/Basic.lean
chore(CategoryTheory/Monad): rename `η'` to `η` (#14886) …
Deleted CategoryTheory.Comonad.left_counitView on Github →
2023-03-24 13:50
Mathlib/CategoryTheory/Monad/Basic.lean
feat: port CategoryTheory.Monad.Basic (#2969)
Added CategoryTheory.Comonad.left_counitView on Github →