Def CategoryTheory.Comonad.Simps.coe

Modification history

2024-07-20 03:37

Mathlib/CategoryTheory/Monad/Basic.lean

chore(CategoryTheory/Monad): rename `η'` to `η` (#14886) …

Deleted CategoryTheory.Comonad.Simps.coe View on Github →

2023-03-24 13:50

Mathlib/CategoryTheory/Monad/Basic.lean

feat: port CategoryTheory.Monad.Basic (#2969)

Added CategoryTheory.Comonad.Simps.coe View on Github →