Theorem div_mul_eq_div_mul_one_div

Modification history