Theorem smul_mul_smul

Modification history