algebra): lint and golf (#8160)

Commit

4 years ago

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

Author

b-mehta

Parents