Commit 2022-12-09 01:07 300aa6fc

View on Github →

feat: port Algebra.GroupWithZero.Units.Lemmas (#920) Port of Algebra.GroupWithZero.Units.Lemmas based on 4dc134b97a3de65ef2ed881f3513d56260971562

Estimated changes

added theorem Units.smul_mk0
added theorem div_div_cancel'
added theorem div_eq_div_iff
added theorem div_eq_iff
added theorem div_eq_iff_mul_eq
added theorem div_eq_of_eq_mul
added theorem div_eq_one_iff_eq
added theorem div_helper
added theorem div_left_inj'
added theorem div_mul_cancel
added theorem div_mul_cancel_of_imp
added theorem div_mul_div_cancel
added theorem div_mul_left
added theorem div_mul_right
added theorem div_self
added theorem divp_mk0
added theorem eq_div_iff
added theorem eq_div_iff_mul_eq
added theorem eq_div_of_mul_eq
added theorem eq_on_inv₀
added theorem inv_mul_eq_one₀
added theorem map_div₀
added theorem map_eq_zero
added theorem map_inv₀
added theorem map_ne_zero
added theorem mul_div_cancel'
added theorem mul_div_cancel
added theorem mul_div_cancel_left
added theorem mul_div_cancel_of_imp'
added theorem mul_div_cancel_of_imp
added theorem mul_div_mul_left
added theorem mul_div_mul_right
added theorem mul_inv_eq_one₀
added theorem mul_mul_div
added theorem mul_one_div_cancel
added theorem one_div_mul_cancel