mathlib3

feat(ring_theory/algebra_operations): multiplication of submodules of an algebra

#658

Merged