Theorem UniqueFactorizationMonoid.prime_pow_coprime_prod_of_coprime_insert

Modification history