Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-15 04:20 53e5dd30

View on Github →

chore(category/limits/opposites): instances (#16511) Upgrade some lemmas to instances, per zulip.

Estimated changes

Modified src/algebraic_geometry/AffineScheme.lean

Modified src/algebraic_geometry/pullbacks.lean

Modified src/category_theory/abelian/generator.lean

Modified src/category_theory/abelian/opposite.lean

Modified src/category_theory/generator.lean

Modified src/category_theory/limits/opposites.lean

deleted theorem category_theory.limits.has_coequalizers_opposite

deleted theorem category_theory.limits.has_colimits_op_of_has_limits

deleted theorem category_theory.limits.has_coproducts_opposite

deleted theorem category_theory.limits.has_equalizers_opposite

deleted theorem category_theory.limits.has_finite_colimits_opposite

deleted theorem category_theory.limits.has_finite_coproducts_opposite

deleted theorem category_theory.limits.has_finite_limits_opposite

deleted theorem category_theory.limits.has_finite_products_opposite

deleted theorem category_theory.limits.has_limits_op_of_has_colimits

deleted theorem category_theory.limits.has_products_opposite

deleted theorem category_theory.limits.has_pullbacks_opposite

deleted theorem category_theory.limits.has_pushouts_opposite