mathlib

a7b660e4 - feat(linear_algebra/prod): add coprod_map_prod (#8220)

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.