Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-14 21:59 65db9668

View on Github →

feat(algebra/field): more division lemmas

Estimated changes

Modified algebra/big_operators.lean

added theorem finset.single_le_sum

Modified algebra/field.lean

deleted theorem abs_inv

added theorem add_div

added theorem div_div_cancel

added theorem div_div_div_cancel_right

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

modified theorem division_ring.inv_comm_of_comm

deleted theorem division_ring.inv_div

added theorem division_ring.inv_eq_iff

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_div_div_cancel_right

added theorem field.div_mul_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

Modified algebra/functions.lean

added def abs_add

Modified algebra/group.lean

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.inv_mul_cancel_left

added theorem units.inv_mul_cancel_right

added theorem units.mul_coe

added theorem units.mul_inv

added theorem units.mul_inv_cancel_left

added theorem units.mul_inv_cancel_right

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

Modified algebra/group_power.lean

Modified algebra/linear_algebra/basic.lean

deleted theorem is_submodule_span

Modified algebra/module.lean

Modified algebra/order.lean

added theorem exists_ge_of_linear

Created algebra/ordered_field.lean

added theorem abs_inv

added theorem div_le_div_left

added theorem div_le_div_right

added theorem div_le_div_right_of_neg

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_div_right_of_neg

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

Modified algebra/ordered_group.lean

Modified algebra/ordered_ring.lean

added theorem lt_add_one

modified theorem one_lt_two

Modified algebra/ring.lean

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