mathlib3

ade1ee30 - feat(category_theory/limits): derive has_binary_products from has_limit (pair X Y) (#2139)

feat(category_theory/limits): derive has_binary_products from has_limit (pair X Y) (#2139) * feat(category_theory/limits): derive has_binary_products from has_limit (pair X Y) * Rename *_of_diagram to diagram_iso_* Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>