Mathlib v3 is deprecated. Go to Mathlib v4

Theorem submodule.sum_smul_mem

Modification history

2020-08-06 15:42

src/algebra/module/basic.lean

chore(algebra/module): Move submodule to its own file (#3696)

Modified submodule.sum_smul_mem View on Github →

2020-07-20 09:41

src/algebra/module.lean

feat (algebra/module): lemma about submodules (#3466) …

Added submodule.sum_smul_mem View on Github →