Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-16 02:53 a1c3e2de

View on Github →

feat(algebra): new algebra theorems (more iff)

Estimated changes

Modified algebra/big_operators.lean

Created algebra/functions.lean

added theorem abs_eq_zero

added theorem abs_le

added theorem abs_lt

added theorem le_min_iff

added theorem max_le_iff

Modified algebra/group.lean

deleted theorem abs_eq_zero_iff

deleted theorem abs_le_iff

deleted theorem abs_lt_iff

added theorem add_sub_cancel'

added theorem add_sub_cancel'_right

deleted theorem eq_iff_sub_eq_zero

modified theorem eq_inv_iff_eq_inv

added theorem eq_inv_mul_iff_mul_eq

added theorem eq_mul_inv_iff_mul_eq

added theorem eq_of_inv_eq_inv

deleted theorem eq_of_mul_inv_eq_one

deleted theorem eq_one_of_inv_eq_one

added theorem eq_sub_iff_add_eq'

modified theorem eq_sub_iff_add_eq

added theorem inv_eq_iff_inv_eq

deleted theorem inv_eq_inv_iff_eq

added theorem inv_eq_one

deleted theorem inv_eq_one_iff_eq_one

added theorem inv_inj'

added theorem inv_mul_eq_iff_eq_mul

added theorem inv_ne_one

modified theorem le_sub_iff_add_le

modified theorem left_inverse_inv

deleted theorem mul_eq_iff_eq_inv_mul

deleted theorem mul_eq_iff_eq_mul_inv

added theorem mul_eq_one_iff_eq_inv

added theorem mul_eq_one_iff_inv_eq

added theorem mul_inv_eq_iff_eq_mul

added theorem mul_inv_eq_one

added theorem mul_left_inj

added theorem mul_right_inj

added theorem mul_self_iff_eq_one

added theorem neg_add'

added theorem sub_add_sub_cancel

added theorem sub_eq_iff_eq_add'

modified theorem sub_eq_iff_eq_add

added theorem sub_eq_neg_add

added theorem sub_eq_zero

modified theorem sub_le_iff_le_add

added theorem sub_left_inj

added theorem sub_ne_zero

added theorem sub_right_inj

added theorem sub_sub_sub_cancel_left

added theorem sub_sub_sub_cancel_right

added theorem sub_sub_swap

Created algebra/order.lean

added theorem eq_of_forall_ge_iff

added theorem eq_of_forall_le_iff

added theorem le_iff_eq_or_lt

added theorem le_iff_le_iff_lt_iff_lt

added theorem le_imp_le_iff_lt_imp_lt

added theorem le_of_not_lt

added theorem not_le

added theorem not_le_of_lt

added theorem not_lt

added theorem not_lt_iff_eq_or_lt

added theorem not_lt_of_le

added theorem not_lt_of_lt

Created algebra/ordered_group.lean

added theorem add_eq_zero_iff_eq_zero_of_nonneg

added theorem add_le_add_iff_left

added theorem add_le_add_iff_right

added theorem add_lt_add_iff_left

added theorem add_lt_add_iff_right

added theorem le_add_iff_nonneg_left

added theorem le_add_iff_nonneg_right

added theorem le_neg

added theorem le_neg_add_iff_add_le

added theorem le_sub_left_iff_add_le

added theorem le_sub_right_iff_add_le

added theorem lt_add_iff_pos_left

added theorem lt_add_iff_pos_right

added theorem lt_neg

added theorem lt_neg_add_iff_add_lt

added theorem lt_sub_left_iff_add_lt

added theorem lt_sub_right_iff_add_lt

added theorem neg_add_le_iff_le_add

added theorem neg_add_le_iff_le_add_right

added theorem neg_add_lt_iff_lt_add

added theorem neg_add_lt_iff_lt_add_right

added theorem neg_le

added theorem neg_le_neg_iff

added theorem neg_le_sub_iff_le_add

added theorem neg_le_sub_iff_le_add_left

added theorem neg_lt

added theorem neg_lt_neg_iff

added theorem neg_lt_sub_iff_lt_add

added theorem neg_lt_sub_iff_lt_add_left

added theorem neg_lt_zero

added theorem neg_nonneg

added theorem neg_nonpos

added theorem neg_pos

added theorem nonneg_comm_group.nonneg_def

added theorem nonneg_comm_group.nonneg_total_iff

added theorem nonneg_comm_group.not_zero_pos

added theorem nonneg_comm_group.pos_def

added def nonneg_comm_group.to_decidable_linear_ordered_comm_group

added theorem nonneg_comm_group.zero_lt_iff_nonneg_nonneg

added theorem sub_le

added theorem sub_le_self_iff

added theorem sub_le_sub_iff_left

added theorem sub_le_sub_iff_right

added theorem sub_left_le_iff_le_add

added theorem sub_left_lt_iff_lt_add

added theorem sub_lt

added theorem sub_lt_self_iff

added theorem sub_lt_sub_iff_left

added theorem sub_lt_sub_iff_right

added theorem sub_lt_zero

added theorem sub_nonneg

added theorem sub_nonpos

added theorem sub_pos

added theorem sub_right_le_iff_le_add

added theorem sub_right_lt_iff_lt_add

Created algebra/ordered_ring.lean

added theorem le_mul_iff_one_le_left

added theorem le_mul_iff_one_le_right

added theorem le_mul_of_ge_one_left'

added theorem le_mul_of_ge_one_right'

added theorem linear_ordered_ring.eq_zero_or_eq_zero_of_mul_eq_zero

added theorem lt_mul_iff_one_lt_left

added theorem lt_mul_iff_one_lt_right

added theorem lt_mul_of_gt_one_right'

added theorem mul_le_mul_left

added theorem mul_le_mul_left_of_neg

added theorem mul_le_mul_right

added theorem mul_le_mul_right_of_neg

added theorem mul_lt_mul_left

added theorem mul_lt_mul_left_of_neg

added theorem mul_lt_mul_right

added theorem mul_lt_mul_right_of_neg

added def nonneg_ring.nonneg_ring.to_linear_nonneg_ring

Modified algebra/ring.lean

added theorem domain.mul_left_inj

added theorem domain.mul_right_inj

added theorem dvd_neg

modified theorem eq_of_mul_eq_mul_left_of_ne_zero

modified theorem eq_of_mul_eq_mul_right_of_ne_zero

added theorem eq_zero_of_mul_eq_self_left'

added theorem eq_zero_of_mul_eq_self_right'

added theorem mul_eq_zero

added theorem mul_ne_zero'

added theorem mul_ne_zero_comm'

added theorem mul_two

modified theorem ne_zero_and_ne_zero_of_mul_ne_zero

added theorem neg_dvd

Modified topology/ennreal.lean

Modified topology/metric_space.lean

Modified topology/real.lean