Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-05 21:26 89ada87c

View on Github →

chore(algebra, data/pnat): refactoring comm_semiring_has_dvd into comm_monoid_has_dvd (#3702) changes the instance comm_semiring_has_dvd to apply to any comm_monoid cleans up the pnat API to use this new definition

Estimated changes

added theorem dvd.elim
added theorem dvd.elim_left
added theorem dvd.intro
added theorem dvd.intro_left
added theorem dvd_mul_left
added theorem dvd_mul_of_dvd_left
added theorem dvd_mul_of_dvd_right
added theorem dvd_mul_right
added theorem dvd_of_mul_left_dvd
added theorem dvd_of_mul_right_dvd
added theorem dvd_refl
added theorem dvd_trans
added theorem dvd_zero
added theorem eq_zero_of_zero_dvd
added theorem mul_dvd_mul
added theorem mul_dvd_mul_left
added theorem mul_dvd_mul_right
added theorem one_dvd
added theorem zero_dvd_iff
deleted theorem dvd.elim
deleted theorem dvd.elim_left
deleted theorem dvd.intro
deleted theorem dvd.intro_left
deleted theorem dvd_mul_left
deleted theorem dvd_mul_of_dvd_left
deleted theorem dvd_mul_of_dvd_right
deleted theorem dvd_mul_right
deleted theorem dvd_of_mul_left_dvd
deleted theorem dvd_of_mul_right_dvd
deleted theorem dvd_refl
deleted theorem dvd_trans
deleted theorem dvd_zero
deleted theorem eq_zero_of_zero_dvd
deleted theorem exists_eq_mul_left_of_dvd
deleted theorem mul_dvd_mul
deleted theorem mul_dvd_mul_left
deleted theorem mul_dvd_mul_right
deleted theorem one_dvd
deleted theorem zero_dvd_iff
deleted theorem pnat.dvd_iff''
modified theorem pnat.dvd_iff
deleted theorem pnat.dvd_intro
modified theorem pnat.dvd_lcm_left
modified theorem pnat.dvd_lcm_right
deleted theorem pnat.dvd_refl
modified theorem pnat.gcd_dvd_left
modified theorem pnat.gcd_dvd_right
deleted theorem pnat.one_dvd