Theorem mul_left_injective₀

Modification history