mathlib3

eb3c0077 - Removed 0 < k from `prime_factorization_prime_pos_pow`