Commit 2020-11-13 17:59 eeb20575
View on Github →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