Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-11 09:57 f92fd0d1

View on Github →

refactor(algebra/divisibility, associated): generalize instances in divisibility, associated (#3714) generalizes the divisibility relation to noncommutative monoids adds missing headers to algebra/divisibility generalizes the instances in many of the lemmas in algebra/associated reunites (some of the) divisibility API for ordinals with general monoids

Estimated changes

modified theorem associated_of_dvd_dvd
modified theorem dvd_dvd_iff_associated
modified theorem dvd_dvd_of_associated
modified theorem dvd_iff_dvd_of_rel_left
deleted theorem dvd_mul_unit_iff
modified theorem dvd_of_associated
modified theorem dvd_symm_iff_of_irreducible
modified theorem dvd_symm_of_irreducible
modified theorem irreducible.ne_zero
modified theorem is_unit_iff_dvd_one
modified theorem is_unit_iff_forall_dvd
modified theorem is_unit_of_dvd_one
modified theorem is_unit_of_dvd_unit
deleted theorem mul_dvd_of_is_unit_left
deleted theorem mul_dvd_of_is_unit_right
deleted theorem mul_unit_dvd_iff
modified theorem not_irreducible_zero
modified theorem not_prime_one
modified theorem not_prime_zero
modified theorem prime.div_or_div
modified theorem prime.dvd_of_dvd_pow
modified theorem prime.ne_zero
modified theorem prime.not_unit
modified def prime
deleted theorem unit_mul_dvd_iff
modified theorem dvd_mul_left
added theorem is_unit.dvd
added theorem is_unit.dvd_mul_left
added theorem is_unit.dvd_mul_right
added theorem is_unit.mul_left_dvd
added theorem is_unit.mul_right_dvd
added theorem mul_dvd_mul_iff_left
modified theorem one_dvd
added theorem units.coe_dvd
added theorem units.dvd_mul_left
added theorem units.dvd_mul_right
added theorem units.mul_left_dvd
added theorem units.mul_right_dvd
modified theorem pow_dvd_pow
modified theorem pow_dvd_pow_of_dvd
modified theorem pow_eq_zero
modified theorem pow_ne_zero
modified theorem zero_pow
deleted theorem mul_dvd_mul_iff_left
modified theorem two_dvd_bit1
deleted theorem units.coe_dvd
deleted theorem units.coe_mul_dvd
deleted theorem units.coe_ne_zero
deleted theorem units.dvd_coe
deleted theorem units.dvd_coe_mul
deleted theorem ordinal.dvd_def
deleted theorem ordinal.dvd_mul
deleted theorem ordinal.dvd_mul_of_dvd
deleted theorem ordinal.dvd_trans