Commit 2022-06-15 00:05 2e2d5155
View on Github →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.