Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-22 09:45 928496ad

View on Github →

feat(category_theory/limits) Binary product from pullbacks and terminal object (#1998)

  • Binary product from pullbacks and terminal object
  • Update binary_products.lean
  • simplifications
  • pare down the proof a bit more
  • changes from review
  • adjust simp to rw

Estimated changes