mathlib3
1a398a72 - docs(category_theory/limits): adding many docstrings (#2185)

Commit
5 years ago
docs(category_theory/limits): adding many docstrings (#2185) * lots of comments! * remove #lint * Apply suggestions from code review lots of missing "co"s Co-Authored-By: Johan Commelin <johan@commelin.net> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Author
Parents
Loading