Theorem UniqueFactorizationMonoid.prime_of_normalized_factor

Modification history