Commit 2022-05-10 11:03 91489acb

feat(algebra/module/submodule_bilinear): add submodule.map₂, generalizing submodule.has_mul (#13709) The motivation here is to be able to talk about combinations of submodules under other bilinear maps, such as the tensor product. This unifies the definitions of and lemmas about submodule.has_mul and submodule.has_scalar'. The lemmas about submodule.map₂ are copied verbatim from those for mul, and then adjusted slightly replacing mul_zero with linear_map.map_zero etc. I've then replaced the lemmas about smul with the map₂ proofs where possible. The lemmas about finiteness weren't possible to copy this way, as the proofs about finset multiplication are not generalized in a similar way. Someone else can copy these in a future PR. This also adds set.image2_eq_Union to match set.image_eq_Union, and removes submodule.union_eq_smul_set which is neither about submodules nor about union, and instead is really just a copy of set.image_eq_Union