Commit 2022-11-15 02:10 d5d94ecd
View on Github →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.
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.