Commit 2020-10-25 16:45 69f550cb

chore(ring_theory/unique_factorization_domain): fix some lemma names (#4765) Fixes names of some lemmas that were erroneously renamed with find-and-replace Changes some constructor names to use dot notation Names replaced: exists_prime_of_factor -> exists_prime_factors wf_dvd_monoid_of_exists_prime_of_factor -> wf_dvd_monoid.of_exists_prime_factors irreducible_iff_prime_of_exists_prime_of_factor -> irreducible_iff_prime_of_exists_prime_factors unique_factorization_monoid_of_exists_prime_of_factor -> unique_factorization_monoid.of_exists_prime_factors unique_factorization_monoid_iff_exists_prime_of_factor -> unique_factorization_monoid.iff_exists_prime_factors irreducible_iff_prime_of_exists_unique_irreducible_of_factor -> irreducible_iff_prime_of_exists_unique_irreducible_factors unique_factorization_monoid.of_exists_unique_irreducible_of_factor -> unique_factorization_monoid.of_exists_unique_irreducible_factors no_factors_of_no_prime_of_factor -> no_factors_of_no_prime_factors dvd_of_dvd_mul_left_of_no_prime_of_factor -> dvd_of_dvd_mul_left_of_no_prime_factors dvd_of_dvd_mul_right_of_no_prime_of_factor -> dvd_of_dvd_mul_right_of_no_prime_factors