Mathlib v3 is deprecated. Go to Mathlib v4

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

Modified src/category_theory/abelian/basic.lean

Renamed src/category_theory/limits/shapes/constructions/binary_products.lean to src/category_theory/limits/constructions/binary_products.lean

Renamed src/category_theory/limits/shapes/constructions/equalizers.lean to src/category_theory/limits/constructions/equalizers.lean

Renamed src/category_theory/limits/shapes/constructions/limits_of_products_and_equalizers.lean to src/category_theory/limits/constructions/limits_of_products_and_equalizers.lean

Renamed src/category_theory/limits/shapes/constructions/over/connected.lean to src/category_theory/limits/constructions/over/connected.lean

modified def category_theory.over.creates_connected.raised_cone_is_limit

Renamed src/category_theory/limits/shapes/constructions/over/default.lean to src/category_theory/limits/constructions/over/default.lean

Renamed src/category_theory/limits/shapes/constructions/over/products.lean to src/category_theory/limits/constructions/over/products.lean

modified def category_theory.over.construct_products.cones_equiv

modified def category_theory.over.construct_products.cones_equiv_counit_iso

modified def category_theory.over.construct_products.cones_equiv_unit_iso

modified theorem category_theory.over.construct_products.has_over_limit_discrete_of_wide_pullback_limit

modified theorem category_theory.over.construct_products.over_product_of_wide_pullback

modified def category_theory.over.construct_products.wide_pullback_diagram_of_diagram_over

Renamed src/category_theory/limits/shapes/constructions/pullbacks.lean to src/category_theory/limits/constructions/pullbacks.lean

Modified src/order/category/omega_complete_partial_order.lean