Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-10 17:41 3424a593

View on Github →

chore(category_theory/limits/*): Unify names for limit constructions. (#15810) List of renames: limits_from_equalizers_and_products -> has_limits_of_has_equalizers_and_products colimits_from_coequalizers_and_coproducts -> has_colimits_of_has_coequalizers_and_coproducts finite_limits_from_equalizers_and_finite_products -> has_finite_limits_of_has_equalizers_and_finite_products finite_colimits_from_coequalizers_and_finite_coproducts -> has_finite_colimits_of_has_coequalizers_and_finite_coproducts has_binary_products_of_terminal_and_pullbacks -> has_binary_products_of_has_terminal_and_pullbacks has_binary_coproducts_of_initial_and_pushouts -> has_binary_coproducts_of_has_initial_and_pushouts has_equalizers_of_pullbacks_and_binary_products -> has_equalizers_of_has_pullbacks_and_binary_products has_coequalizers_of_pushouts_and_binary_coproducts -> has_coequalizers_of_has_pushouts_and_binary_coproducts preserves_equalizers_of_pullbacks_and_binary_products -> preserves_equalizers_of_preserves_pullbacks_and_binary_products preserves_coequalizers_of_pushouts_and_binary_coproducts -> preserves_coequalizers_of_preserves_pushouts_and_binary_coproducts has_finite_coproducts_of_has_binary_and_terminal -> has_finite_coproducts_of_has_binary_and_initial

Estimated changes