Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-08 12:44 94cbfad7

View on Github →

chore(algebra/*): move some lemmas about is_unit from associated.lean (#12526) There doesn't seem to be any reason for them to live there.

Estimated changes

deleted theorem dvd_and_not_dvd_iff
deleted theorem is_unit_iff_dvd_one
deleted theorem is_unit_iff_forall_dvd
deleted theorem is_unit_of_dvd_one
deleted theorem is_unit_of_dvd_unit
deleted theorem pow_dvd_pow_iff
added theorem dvd_and_not_dvd_iff
added theorem is_unit_iff_dvd_one
added theorem is_unit_iff_forall_dvd
added theorem is_unit_of_dvd_one
added theorem is_unit_of_dvd_unit
added theorem pow_dvd_pow_iff