mathlib

eeb20575 - feat(ring_theory/unique_factorization_domain): connecting `multiplicity` to `unique_factorization_domain.factors` (#4980)

feat(ring_theory/unique_factorization_domain): connecting `multiplicity` to `unique_factorization_domain.factors` (#4980) Connects multiplicity of an irreducible to the multiset of irreducible factors Co-authored-by: jalex-stark <alexmaplegm@gmail.com>