Commit 2021-01-12 08:26 cd7a8a18

View on Github →

chore(category_theory/limits): move constructions folder (#5681) As mentioned here: https://github.com/leanprover-community/mathlib/pull/5516#issuecomment-753450199 The linter is giving new errors, so I might as well fix them in this PR.

Estimated changes