Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-01 20:17 4e7c6b27

View on Github →

chore(algebra/associated): weaken some typeclass assumptions (#7760) Also golf ne_zero_iff_of_associated a little.

Estimated changes

modified theorem dvd_iff_dvd_of_rel_left
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