Theorem smul_eq_mul

Modification history