mathlib

4e8d8f27 - feat(ring_theory/unique_factorization_domain): factors of `p^k` (#12369)

feat(ring_theory/unique_factorization_domain): factors of `p^k` (#12369) This is a relatively trivial application of existing lemmas, but the result is a particularly nice shape that I felt worth to add to the library. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>