mathlib

2e2d5155 - feat(data/nat/factorization): add lemma `coprime_of_div_pow_factorization` (#14576)

feat(data/nat/factorization): add lemma `coprime_of_div_pow_factorization` (#14576) Add lemma `coprime_of_div_pow_factorization (hp : prime p) (hn : n ≠ 0) : coprime p (n / p ^ n.factorization p)` Prompted by [this Zulip question](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/div.20by.20p_adic_val_nat.20is.20coprime).