Def CategoryTheory.Monad.Simps.η

Modification history

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