mathlib

69f550cb - chore(ring_theory/unique_factorization_domain): fix some lemma names (#4765)

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`