Theorem UniqueFactorizationMonoid.normalizedFactors_pos

Modification history