Theorem AddSubmonoid.smul_le_smul

Modification history