Theorem UniqueFactorizationMonoid.exists_mem_normalizedFactors

Modification history