mathlib3
e14d5eba - feat(category_theory/limits): prod map is iso if components are (#5620)

Commit

5 years ago

feat(category_theory/limits): prod map is iso if components are (#5620) Show that if `f` and `g` are iso, then `prod.map f g` is an iso, and the dual.

Author

b-mehta

Parents

87ef7aff

mathlib3 e14d5eba - feat(category_theory/limits): prod map is iso if components are (#5620)

mathlib3
e14d5eba - feat(category_theory/limits): prod map is iso if components are (#5620)