Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-14 20:17 1a3c0696

View on Github →

chore(data/equiv/set): more lemmas about prod (#12022) Note we don't need the symm lemmas for prod.comm, since prod.comm is involutive

Estimated changes

Modified src/data/equiv/set.lean

added theorem equiv.prod_assoc_image

added theorem equiv.prod_assoc_symm_image

added theorem equiv.prod_assoc_symm_preimage

added theorem equiv.prod_comm_image

added theorem equiv.prod_comm_preimage