Theorem smul_inv_smul

Modification history