Commit 2018-01-14 21:59 65db9668

View on Github →

feat(algebra/field): more division lemmas

Estimated changes

deleted theorem abs_inv
added theorem add_div
added theorem div_div_cancel
added theorem div_eq_div_iff
added theorem div_eq_mul_inv
added theorem div_eq_zero_iff
deleted theorem div_le_iff_le_mul_of_pos
added theorem div_mul_comm
added theorem div_mul_div_cancel
added theorem div_ne_zero
added theorem div_ne_zero_iff
added theorem div_neg
added theorem div_right_comm
added theorem div_right_inj
deleted theorem division_ring.inv_div
added theorem division_ring.inv_inj
deleted theorem division_ring.neg_inv
added theorem divp_eq_div
added theorem divp_mk0
added theorem field.div_div_cancel
added theorem field.div_right_comm
added theorem inv_add_inv
added theorem inv_div
added theorem inv_div_left
deleted theorem inv_le_inv
deleted theorem inv_lt_one
deleted theorem inv_neg
deleted theorem inv_pos
added theorem inv_sub_inv
deleted theorem ivl_stretch
deleted theorem ivl_translate
deleted theorem le_div_iff_mul_le_of_pos
deleted theorem lt_div_iff
added theorem mul_comm_div
added theorem mul_div_comm
added theorem mul_div_right_comm
added theorem neg_inv
deleted theorem one_lt_inv
added theorem sub_div
added theorem units.inv_eq_inv
added def units.mk0
added theorem units.mk0_inv
added theorem units.mk0_val
added theorem units.ne_zero
added def divp
added theorem divp_assoc
added theorem divp_eq_one
added theorem divp_mul_cancel
added theorem divp_one
added theorem divp_right_inj
added theorem divp_self
added theorem mul_divp_cancel
modified theorem mul_left_inj
modified theorem mul_right_inj
added theorem one_divp
added theorem units.ext
added theorem units.inv_coe
added theorem units.inv_mul
added theorem units.mul_coe
added theorem units.mul_inv
added theorem units.mul_left_inj
added theorem units.mul_right_inj
added theorem units.one_coe
added theorem units.val_coe
added structure units
added theorem abs_inv
added theorem div_le_div_left
added theorem div_le_div_right
added theorem div_le_iff
added theorem div_le_iff_of_neg
added theorem div_le_one_iff_le
added theorem div_lt_div'
added theorem div_lt_div
added theorem div_lt_div_iff
added theorem div_lt_div_left
added theorem div_lt_div_right
added theorem div_lt_iff
added theorem div_lt_iff_of_neg
added theorem div_lt_one_iff_lt
added def div_nonneg
added def div_pos
added def half_lt_self
added theorem half_pos
added theorem inv_le_inv'
added theorem inv_le_inv
added theorem inv_lt_inv
added theorem inv_lt_one
added theorem inv_neg
added theorem inv_pos
added theorem ivl_stretch
added theorem ivl_translate
added theorem le_div_iff
added theorem lt_div_iff
added theorem one_div_le_one_div
added theorem one_div_lt_one_div
added theorem one_le_div_iff_le
added theorem one_lt_div_iff_lt
added theorem one_lt_inv
deleted theorem add_div
deleted theorem div_eq_mul_inv
deleted theorem neg_inv
deleted theorem units.ext
deleted theorem units.inv_coe
deleted theorem units.inv_mul
deleted theorem units.mul_coe
deleted theorem units.mul_inv
deleted theorem units.one_coe
deleted theorem units.val_coe
deleted structure units