Commit 2021-07-06 18:26 d7653b8d

View on Github →

chore(category_theory/monad/algebra): lint and golf (#8160) Adds a module docstring and golfs some proofs, including removing erw.

Estimated changes

Modified src/category_theory/monad/algebra.lean

modified def category_theory.comonad.coalgebra.iso_mk

modified def category_theory.monad.algebra.iso_mk

Modified src/category_theory/monad/limits.lean

modified def category_theory.monad.forget_creates_limits.new_cone

modified def category_theory.monad.forget_creates_limits.γ