Commit 2022-04-08 06:14 ccf3e37f

feat(ring_theory/unique_factorization_domain): alternative specification for count (normalized_factors x) (#13161) count_normalized_factors_eq specifies the number of times an irreducible factor p appears in normalized_factors x, namely the number of times it divides x. This is often easier to work with than going through multiplicity since this way we avoid coercing to enat.