mathlib
744d59af - refactor(category_theory/limits): split file (#6751)

Commit
4 years ago
refactor(category_theory/limits): split file (#6751) This splits `category_theory.limits.limits` into `category_theory.limits.is_limit` and `category_theory.limits.has_limits`. It doesn't meaningfully reduce imports, as everything imports `has_limits`, but in principle it could, and hopefully it makes the content slightly easier to understand when separated. In any case, the file was certainly too large. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading