Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-01 04:50 551cf8e2

View on Github →

refactor(algebra/associates): unite associates.prime with prime (#3988) deletes associates.prime, replaces it with the existing prime

Estimated changes

added theorem associates.mk_dvd_mk
deleted theorem associates.prime.ne_one
deleted theorem associates.prime.ne_zero
deleted def associates.prime
modified theorem dvd_iff_dvd_of_rel_right
modified theorem eq_zero_iff_of_associated
modified theorem irreducible_of_associated
modified theorem ne_zero_iff_of_associated
added theorem prime.ne_one
modified theorem prime_iff_of_associated
modified theorem prime_of_associated