mathlib3

ccf3e37f - feat(ring_theory/unique_factorization_domain): alternative specification for `count (normalized_factors x)` (#13161)

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`.