Commit 2022-03-26 12:20 5e449c20

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