mathlib

8c89ae6f - feat(ring_theory/unique_factorization_domain): some lemmas relating shapes of factorisations (#9345)

feat(ring_theory/unique_factorization_domain): some lemmas relating shapes of factorisations (#9345) Given elements `a`, `b` in a `unique_factorization_monoid`, if there is an order-preserving bijection between the sets of factors of `associates.mk a` and `associates.mk b` then the prime factorisations of `a` and `b` have the same shape. Co-authored-by: Johan Commelin <johan@commelin.net>