Theorem HasCompactMulSupport.comp_smul

Modification history