Theorem UniqueFactorizationMonoid.normalizedFactors_mul

Modification history