Commit 2021-07-07 08:47 06f0d517

View on Github →

refactor(algebra/ordered_group): another step in the order refactor -- ordered groups (#8060) This PR represents another wave of generalization of proofs, following from the order refactor. It is another step towards #7645.

Estimated changes

Modified src/algebra/ordered_group.lean

modified def abs

modified theorem abs_eq_abs

added theorem div_le''

added theorem div_le_div''

added theorem div_le_div_flip

added theorem div_le_div_iff'

added theorem div_le_div_iff_left

added theorem div_le_div_iff_right

added theorem div_le_div_left'

added theorem div_le_div_right'

added theorem div_le_iff_le_mul'

added theorem div_le_iff_le_mul

added theorem div_le_inv_mul_iff

added theorem div_le_one'

added theorem div_lt''

added theorem div_lt_div''

added theorem div_lt_div_iff'

added theorem div_lt_div_iff_left

added theorem div_lt_div_iff_right

added theorem div_lt_div_left'

added theorem div_lt_div_right'

added theorem div_lt_iff_lt_mul'

added theorem div_lt_iff_lt_mul

added theorem div_lt_one'

modified theorem eq_or_eq_neg_of_abs_eq

modified def function.injective.ordered_comm_group

deleted theorem inv_inv_of_one_lt

added theorem inv_le_div_iff_le_mul'

added theorem inv_le_div_iff_le_mul

modified theorem inv_le_inv'

deleted theorem inv_le_one'

modified theorem inv_le_one_of_one_le

deleted theorem inv_le_self

added theorem inv_lt_div_iff_lt_mul'

added theorem inv_lt_div_iff_lt_mul

modified theorem inv_lt_inv'

deleted theorem inv_lt_one'

deleted theorem inv_lt_one_iff_one_lt

added theorem inv_lt_one_of_one_lt

deleted theorem inv_lt_self

deleted theorem inv_mul_le_left_of_le_mul

deleted theorem inv_mul_le_of_le_mul

added theorem inv_mul_le_one_iff

deleted theorem inv_mul_le_right_of_le_mul

added theorem inv_mul_lt_iff_lt_mul'

deleted theorem inv_mul_lt_iff_lt_mul_right

deleted theorem inv_mul_lt_left_of_lt_mul

deleted theorem inv_mul_lt_of_lt_mul

added theorem inv_mul_lt_one_iff

added theorem inv_mul_lt_one_iff_lt

deleted theorem inv_mul_lt_right_of_lt_mul

deleted theorem inv_of_one_lt_inv

added theorem le_div''

added theorem le_div_iff_mul_le'

added theorem le_div_iff_mul_le

added theorem le_iff_forall_one_lt_le_mul

added theorem le_iff_forall_one_lt_lt_mul

deleted theorem le_iff_forall_pos_le_add

deleted theorem le_iff_forall_pos_lt_add

deleted theorem le_inv_iff_mul_le_one'

deleted theorem le_inv_iff_mul_le_one

added theorem le_inv_iff_mul_le_one_left

added theorem le_inv_iff_mul_le_one_right

added theorem le_inv_mul_iff_le

deleted theorem le_inv_mul_of_mul_le

deleted theorem le_inv_of_le_inv

added theorem le_mul_inv_iff_le

added theorem le_mul_inv_iff_mul_le

deleted theorem le_mul_of_inv_mul_le

deleted theorem le_mul_of_inv_mul_le_left

deleted theorem le_mul_of_inv_mul_le_right

added theorem le_of_forall_one_lt_le_mul

added theorem le_of_forall_one_lt_lt_mul

deleted theorem le_of_forall_pos_le_add

deleted theorem le_of_forall_pos_lt_add

deleted theorem le_of_inv_le_inv

deleted theorem le_one_of_one_le_inv

deleted theorem le_sub

deleted theorem le_sub_iff_add_le'

deleted theorem le_sub_iff_add_le

added theorem left.inv_le_one_iff

added theorem left.inv_le_self

added theorem left.inv_lt_one_iff

added theorem left.inv_lt_self

added theorem left.one_le_inv_iff

added theorem left.one_lt_inv_iff

added theorem left.self_le_inv

added theorem left.self_lt_inv

added theorem lt_div''

added theorem lt_div_iff_mul_lt'

added theorem lt_div_iff_mul_lt

added theorem lt_inv_mul_iff_lt

deleted theorem lt_inv_mul_of_mul_lt

added theorem lt_mul_inv_iff_lt

added theorem lt_mul_inv_iff_mul_lt

deleted theorem lt_mul_of_inv_mul_lt

deleted theorem lt_mul_of_inv_mul_lt_left

deleted theorem lt_mul_of_inv_mul_lt_right

deleted theorem lt_of_inv_lt_inv

deleted theorem lt_sub

deleted theorem lt_sub_iff_add_lt'

deleted theorem lt_sub_iff_add_lt

deleted theorem max_one_div_eq_self'

added theorem max_one_div_max_inv_one_eq_self

deleted theorem max_zero_sub_max_neg_zero_eq_self

modified theorem mul_inv_le_iff_le_mul

added theorem mul_inv_le_inv_mul_iff

added theorem mul_inv_le_one_iff

added theorem mul_inv_le_one_iff_le

added theorem mul_inv_lt_iff_le_mul'

added theorem mul_inv_lt_iff_lt_mul

added theorem mul_inv_lt_inv_mul_iff

added theorem mul_inv_lt_mul_inv_iff'

added theorem mul_inv_lt_one_iff

deleted theorem mul_le_of_le_inv_mul

deleted theorem mul_lt_of_lt_inv_mul

deleted theorem neg_le_sub_iff_le_add'

deleted theorem neg_le_sub_iff_le_add

deleted theorem neg_lt_sub_iff_lt_add'

deleted theorem neg_lt_sub_iff_lt_add

added theorem one_le_div'

deleted theorem one_le_inv'

modified theorem one_le_inv_of_le_one

deleted theorem one_le_of_inv_le_one

added theorem one_lt_div'

deleted theorem one_lt_inv'

deleted theorem one_lt_inv_of_inv

deleted theorem one_lt_of_inv_inv

added theorem right.inv_le_one_iff

added theorem right.inv_le_self

added theorem right.inv_lt_one_iff

added theorem right.inv_lt_self

added theorem right.one_le_inv_iff

added theorem right.one_lt_inv_iff

added theorem right.self_le_inv

added theorem right.self_lt_inv

deleted theorem self_le_inv

deleted theorem sub_le

deleted theorem sub_le_iff_le_add'

deleted theorem sub_le_iff_le_add

deleted theorem sub_le_sub

deleted theorem sub_le_sub_flip

deleted theorem sub_le_sub_iff

deleted theorem sub_le_sub_iff_left

deleted theorem sub_le_sub_iff_right

deleted theorem sub_le_sub_left

deleted theorem sub_le_sub_right

deleted theorem sub_lt

deleted theorem sub_lt_iff_lt_add'

deleted theorem sub_lt_iff_lt_add

deleted theorem sub_lt_sub

deleted theorem sub_lt_sub_iff_left

deleted theorem sub_lt_sub_iff_right

deleted theorem sub_lt_sub_left

deleted theorem sub_lt_sub_right

deleted theorem sub_lt_zero

deleted theorem sub_nonneg

deleted theorem sub_nonpos

deleted theorem sub_pos

Modified src/analysis/analytic/basic.lean

Modified src/topology/algebra/ordered/basic.lean