mathlib3

5e449c20 - feat(algebra/is_prime_pow): add `is_prime_pow_iff_factorization_single` (#12167)

feat(algebra/is_prime_pow): add `is_prime_pow_iff_factorization_single` (#12167) Adds lemma `is_prime_pow_iff_factorization_single : is_prime_pow n ↔ ∃ p k : ℕ, 0 < k ∧ n.factorization = finsupp.single p k` Also adds `pow_of_factorization_single` to `data/nat/factorization`