mathlib

91489acb - feat(algebra/module/submodule_bilinear): add `submodule.map₂`, generalizing `submodule.has_mul` (#13709)

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`