Theorem mul_left_cancel₀

Modification history