basic): `coe_prod_comm` (#17510)

Commit

3 years ago

feat(logic/equiv/basic): `coe_prod_comm` (#17510) As a result of this new lemma, `prod_comm_image` and `prod_comm_preimage` are now redundant.

Author

YaelDillies

Parents