Theorem left_ne_zero_of_mul

Modification history