Theorem Submodule.smul_toAddSubmonoid

Modification history