mathlib3
72ce940c - feat(category_theory/limits/of_nat_iso): missing parts of the limits API (#1355)

Commit
6 years ago
feat(category_theory/limits/of_nat_iso): missing parts of the limits API (#1355) * feat(category_theory/limits/of_nat_isp) * Update src/category_theory/limits/limits.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Update src/category_theory/limits/limits.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * use @[reassoc] * fixing after rename * fix renaming
Author
Committer
Parents
Loading