Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-04-05 07:48 e8638a0f

View on Github →

feat(algebra/divisibility/basic): Dot notation aliases (#18698) A few convenience shortcuts for dvd along with some simple nat lemmas. Also

  • Drop neg_dvd_of_dvd/dvd_of_neg_dvd/dvd_neg_of_dvd/dvd_of_dvd_neg in favor of the aforementioned shortcuts.
  • Remove explicit arguments to dvd_neg/neg_dvd.
  • Drop int.of_nat_dvd_of_dvd_nat_abs/int.dvd_nat_abs_of_of_nat_dvd because they are the two directions of int.coe_nat_dvd_left.
  • Move group_with_zero.to_cancel_monoid_with_zero from algebra.group_with_zero.units.basic back to algebra.group_with_zero.basic. It was erroneously moved during the Great Splits.

Estimated changes

added theorem dvd_of_eq
added theorem eq_one_of_mul_left
added theorem eq_one_of_mul_right
added theorem mul_eq_one
added theorem left_eq_mul₀
added theorem mul_eq_left₀
added theorem mul_eq_right₀
added theorem right_eq_mul₀
added theorem dvd_antisymm'
added theorem dvd_antisymm
added theorem eq_of_forall_dvd'
added theorem eq_of_forall_dvd
added theorem add_eq_zero'
deleted theorem add_eq_zero
deleted theorem dvd_add_iff_left
deleted theorem dvd_add_iff_right
modified theorem dvd_add_right
modified theorem dvd_iff_dvd_of_dvd_sub
modified theorem dvd_neg
deleted theorem dvd_neg_of_dvd
deleted theorem dvd_of_dvd_neg
deleted theorem dvd_of_neg_dvd
added theorem dvd_sub_left
added theorem dvd_sub_right
added theorem dvd_sub_self_left
added theorem dvd_sub_self_right
modified theorem neg_dvd
deleted theorem neg_dvd_of_dvd
modified theorem two_dvd_bit1
added theorem nat.lcm_pos
deleted theorem nat.mul_eq_one_iff