Mathlib Changelog
Changelog
About
Github
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