mathlib
3424a593 - chore(category_theory/limits/*): Unify names for limit constructions. (#15810)

Commit
3 years ago
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` Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Author
Parents
Loading