Theorem Nat.prod_primeFactors_gcd_mul_prod_primeFactors_mul

Modification history