Commit 2023-04-12 19:26 4fa401fa

View on Github →

feat: Dot notation aliases (#3303) Match https://github.com/leanprover-community/mathlib/pull/18698 and a bit of https://github.com/leanprover-community/mathlib/pull/18785.

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
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
modified theorem dvd_sub_comm
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 Int.dvd_of_pow_dvd
added theorem Nat.lcm_pos
deleted theorem Nat.mul_eq_one_iff