Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-04 07:42 240f6eb9

View on Github →

feat(category_theory/monad): cleanups in monad algebra (#5193)

Converts the simp normal form for composition of algebra homs to use category notation.
Adds simps where appropriate
Golfs proofs, remove some erw and nonterminal simps
Remove some redundant brackets

Estimated changes

Modified src/category_theory/monad/algebra.lean

added theorem category_theory.comonad.coalgebra.comp_eq_comp

added theorem category_theory.comonad.coalgebra.comp_f

modified def category_theory.comonad.coalgebra.hom.comp

modified def category_theory.comonad.coalgebra.hom.id

added theorem category_theory.comonad.coalgebra.id_eq_id

added theorem category_theory.comonad.coalgebra.id_f

added theorem category_theory.monad.algebra.comp_eq_comp

added theorem category_theory.monad.algebra.comp_f

modified def category_theory.monad.algebra.hom.comp

modified def category_theory.monad.algebra.hom.id

added theorem category_theory.monad.algebra.id_eq_id

added theorem category_theory.monad.algebra.id_f