Commit 2021-07-08 17:14 a7b660e4
View on Github →feat(linear_algebra/prod): add coprod_map_prod (#8220)
This also adds submodule.coe_sup and set.mem_finset_prod. The latter was intended to be used to show submodule.coe_supr, but I didn't really need that and it was hard to prove.