mathlib

aab6d3c7 - feat(data/nat/factorization/prime_pow): lemmas relating `is_prime_pow` and `ord_compl = 1` (#15692)

feat(data/nat/factorization/prime_pow): lemmas relating `is_prime_pow` and `ord_compl = 1` (#15692) Adds lemmas showing that `n` is a prime power iff `ord_compl[p] n = 1` (for some prime `p`). `exists_ord_compl_eq_one_of_is_prime_pow (h : is_prime_pow n) : (∃ p : ℕ, p.prime ∧ ord_compl[p] n = 1)` `is_prime_pow_of_ord_compl_eq_one (hn : n ≠ 1) (pp : p.prime) (h : ord_compl[p] n = 1) : is_prime_pow n`