feat(algebra/associated): simple lemmas and dot notation (#8770)
Introduce
* `prime.exists_mem_finset_dvd`
* `prime.not_dvd_one`
Rename
* `exists_mem_multiset_dvd_of_prime` -> `prime.exists_mem_multiset_dvd`
* `left_dvd_or_dvd_right_of_dvd_prime_mul ` ->`prime.left_dvd_or_dvd_right_of_dvd_mul`