Def category_theory.monad.simps.η

Modification history

2021-04-09 04:34

src/category_theory/monad/basic.lean

feat(tactic/simps): allow composite projections (#7074) …

Added category_theory.monad.simps.η View on Github →