Theorem smul_assoc

Modification history