mathlib3

4dc0814e - feat (algebra/module): lemma about submodules (#3466)

feat (algebra/module): lemma about submodules (#3466) Add a 3-line lemma saying that a linear combination of elements of a submodule is still in that submodule.