Theorem trichotomy_of_mul_eq_mul

Modification history