2020-11-13 17:59
src/ring_theory/unique_factorization_domain.lean
feat(ring_theory/unique_factorization_domain): connecting `multiplicity` to `unique_factorization_domain.factors` (#4980) …
Added unique_factorization_monoid.le_multiplicity_iff_repeat_le_factors