Theorem UniqueFactorizationMonoid.ne_zero_of_mem_factors

Modification history