Theorem Submodule.singleton_smul

Modification history