Theorem commute_rmul_rmul_sq

Modification history