Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-21 21:43 c44f19fe

View on Github →

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

Estimated changes

modified theorem prime.ne_one
modified theorem prime.ne_zero
added theorem prime.not_dvd_one
modified theorem prime.not_unit