mathlib
c8a0bb6b - feat(category_theory/products): missing simp lemmas (#1003)

Commit

6 years ago

feat(category_theory/products): missing simp lemmas (#1003) * feat(category_theory/products): missing simp lemmas * cleanup proofs * fix proof * squeeze_simp

References

#1003 - feat(category_theory/products): missing simp lemmas

Author

kim-em

Committer

mergify[bot]

Parents

6c35df0d

mathlib c8a0bb6b - feat(category_theory/products): missing simp lemmas (#1003)

mathlib
c8a0bb6b - feat(category_theory/products): missing simp lemmas (#1003)