refactor(algebra/is_prime_pow): move lemmas using `factorization` to new file (#14598)
As discussed in [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/squarefree.2C.20is_prime_pow.2C.20and.20factorization/near/285144241).