Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-20 09:41 4dc0814e

View on Github →

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.

Estimated changes