Theorem mul_self_eq_mul_self_iff

Modification history