Commit 2020-06-09 17:36 1a4f0c22

View on Github →

refactor(algebra/ordered_group): multiplicative versions of ordered monoids/groups (#2844) This PR defines multiplicative versions of ordered monoids and groups. It also lints the file.

Estimated changes

Modified src/algebra/group/defs.lean

Modified src/algebra/group/to_additive.lean

Modified src/algebra/ordered_group.lean

deleted theorem add_eq_zero_iff'

deleted theorem add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg

deleted theorem add_eq_zero_iff_eq_zero_of_nonneg

deleted theorem add_le_add'

deleted theorem add_le_add

deleted theorem add_le_add_iff_left

deleted theorem add_le_add_iff_right

deleted theorem add_le_add_left'

deleted theorem add_le_add_left

deleted theorem add_le_add_right'

deleted theorem add_le_add_right

deleted theorem add_le_add_three

deleted theorem add_le_iff_nonpos_left

deleted theorem add_le_iff_nonpos_right

deleted theorem add_le_of_le_neg_add

deleted theorem add_le_of_le_of_nonpos'

deleted theorem add_le_of_le_of_nonpos

deleted theorem add_le_of_nonpos_of_le'

deleted theorem add_le_of_nonpos_of_le

deleted theorem add_lt_add

deleted theorem add_lt_add_iff_left

deleted theorem add_lt_add_iff_right

deleted theorem add_lt_add_left

deleted theorem add_lt_add_of_le_of_lt

deleted theorem add_lt_add_of_lt_of_le

deleted theorem add_lt_add_right

deleted theorem add_lt_iff_neg_left

deleted theorem add_lt_iff_neg_right

deleted theorem add_lt_of_le_of_neg

deleted theorem add_lt_of_lt_neg_add

deleted theorem add_lt_of_lt_of_neg'

deleted theorem add_lt_of_lt_of_neg

deleted theorem add_lt_of_lt_of_nonpos'

deleted theorem add_lt_of_lt_of_nonpos

deleted theorem add_lt_of_neg_of_le

deleted theorem add_lt_of_neg_of_lt'

deleted theorem add_lt_of_neg_of_lt

deleted theorem add_lt_of_nonpos_of_lt'

deleted theorem add_lt_of_nonpos_of_lt

deleted theorem add_neg'

deleted theorem add_neg

deleted theorem add_neg_le_iff_le_add'

deleted theorem add_neg_le_iff_le_add

deleted theorem add_neg_of_neg_of_nonpos'

deleted theorem add_neg_of_neg_of_nonpos

deleted theorem add_neg_of_nonpos_of_neg'

deleted theorem add_neg_of_nonpos_of_neg

deleted theorem add_nonneg'

deleted theorem add_nonneg

deleted theorem add_nonpos'

deleted theorem add_nonpos

deleted theorem add_pos'

deleted theorem add_pos

deleted theorem add_pos_of_nonneg_of_pos'

deleted theorem add_pos_of_nonneg_of_pos

deleted theorem add_pos_of_pos_of_nonneg'

deleted theorem add_pos_of_pos_of_nonneg

modified theorem bit0_pos

modified theorem dist_bdd_within_interval

added theorem inv_inv_of_one_lt

added theorem inv_le'

added theorem inv_le_iff_one_le_mul

added theorem inv_le_inv'

added theorem inv_le_inv_iff

added theorem inv_le_of_inv_le

added theorem inv_le_one'

added theorem inv_le_one_of_one_le

added theorem inv_le_self

added theorem inv_lt'

added theorem inv_lt_inv'

added theorem inv_lt_inv_iff

added theorem inv_lt_of_inv_lt

added theorem inv_lt_one'

added theorem inv_lt_one_iff_one_lt

added theorem inv_mul_le_iff_le_mul'

added theorem inv_mul_le_iff_le_mul

added theorem inv_mul_le_left_of_le_mul

added theorem inv_mul_le_of_le_mul

added theorem inv_mul_le_right_of_le_mul

added theorem inv_mul_lt_iff_lt_mul

added theorem inv_mul_lt_iff_lt_mul_right

added theorem inv_mul_lt_left_of_lt_mul

added theorem inv_mul_lt_of_lt_mul

added theorem inv_mul_lt_right_of_lt_mul

added theorem inv_of_one_lt_inv

deleted theorem le_add_iff_nonneg_left

deleted theorem le_add_iff_nonneg_right

deleted theorem le_add_of_le_of_nonneg'

deleted theorem le_add_of_le_of_nonneg

deleted theorem le_add_of_neg_add_le

deleted theorem le_add_of_neg_add_le_left

deleted theorem le_add_of_neg_add_le_right

deleted theorem le_add_of_nonneg_left'

deleted theorem le_add_of_nonneg_left

deleted theorem le_add_of_nonneg_of_le'

deleted theorem le_add_of_nonneg_of_le

deleted theorem le_add_of_nonneg_right'

deleted theorem le_add_of_nonneg_right

added theorem le_inv'

added theorem le_inv_iff_mul_le_one

added theorem le_inv_mul_iff_mul_le

added theorem le_inv_mul_of_mul_le

added theorem le_inv_of_le_inv

added theorem le_mul_iff_one_le_left'

added theorem le_mul_iff_one_le_right'

added theorem le_mul_of_inv_mul_le

added theorem le_mul_of_inv_mul_le_left

added theorem le_mul_of_inv_mul_le_right

added theorem le_mul_of_le_of_one_le'

added theorem le_mul_of_le_of_one_le

added theorem le_mul_of_one_le_left''

added theorem le_mul_of_one_le_left

added theorem le_mul_of_one_le_of_le'

added theorem le_mul_of_one_le_of_le

added theorem le_mul_of_one_le_right''

added theorem le_mul_of_one_le_right

deleted theorem le_neg

deleted theorem le_neg_add_iff_add_le

deleted theorem le_neg_add_of_add_le

deleted theorem le_neg_iff_add_nonpos

deleted theorem le_neg_of_le_neg

deleted theorem le_of_add_le_add_left

deleted theorem le_of_add_le_add_right

added theorem le_of_inv_le_inv

added theorem le_of_mul_le_mul_left'

added theorem le_of_mul_le_mul_right'

deleted theorem le_of_neg_le_neg

added theorem le_one_of_one_le_inv

deleted theorem lt_add_iff_pos_left

deleted theorem lt_add_iff_pos_right

deleted theorem lt_add_of_le_of_pos

deleted theorem lt_add_of_lt_of_nonneg'

deleted theorem lt_add_of_lt_of_nonneg

deleted theorem lt_add_of_lt_of_pos'

deleted theorem lt_add_of_lt_of_pos

deleted theorem lt_add_of_neg_add_lt

deleted theorem lt_add_of_neg_add_lt_left

deleted theorem lt_add_of_neg_add_lt_right

deleted theorem lt_add_of_nonneg_of_lt'

deleted theorem lt_add_of_nonneg_of_lt

deleted theorem lt_add_of_pos_left

deleted theorem lt_add_of_pos_of_le

deleted theorem lt_add_of_pos_of_lt'

deleted theorem lt_add_of_pos_of_lt

deleted theorem lt_add_of_pos_right

added theorem lt_inv'

added theorem lt_inv_mul_iff_mul_lt

added theorem lt_inv_mul_of_mul_lt

added theorem lt_inv_of_lt_inv

added theorem lt_mul_iff_one_lt_left'

added theorem lt_mul_iff_one_lt_right'

added theorem lt_mul_of_inv_mul_lt

added theorem lt_mul_of_inv_mul_lt_left

added theorem lt_mul_of_inv_mul_lt_right

added theorem lt_mul_of_le_of_one_lt

added theorem lt_mul_of_lt_of_one_le'

added theorem lt_mul_of_lt_of_one_le

added theorem lt_mul_of_lt_of_one_lt'

added theorem lt_mul_of_lt_of_one_lt

added theorem lt_mul_of_one_le_of_lt'

added theorem lt_mul_of_one_le_of_lt

added theorem lt_mul_of_one_lt_left

added theorem lt_mul_of_one_lt_of_le

added theorem lt_mul_of_one_lt_of_lt'

added theorem lt_mul_of_one_lt_of_lt

added theorem lt_mul_of_one_lt_right

deleted theorem lt_neg

deleted theorem lt_neg_add_iff_add_lt

deleted theorem lt_neg_add_of_add_lt

deleted theorem lt_neg_of_lt_neg

deleted theorem lt_of_add_lt_add_left'

deleted theorem lt_of_add_lt_add_left

deleted theorem lt_of_add_lt_add_right'

deleted theorem lt_of_add_lt_add_right

added theorem lt_of_inv_lt_inv

added theorem lt_of_mul_lt_mul_left''

added theorem lt_of_mul_lt_mul_left'

added theorem lt_of_mul_lt_mul_right''

added theorem lt_of_mul_lt_mul_right'

deleted theorem lt_of_neg_lt_neg

deleted theorem monotone.add

deleted theorem monotone.add_const

deleted theorem monotone.add_strict_mono

deleted theorem monotone.const_add

added theorem monotone.const_mul'

added theorem monotone.mul'

added theorem monotone.mul_const'

added theorem monotone.mul_strict_mono'

added theorem mul_eq_one_iff'

added theorem mul_eq_one_iff_eq_one_and_eq_one_of_one_le_of_one_le

added theorem mul_eq_one_iff_eq_one_of_one_le

added theorem mul_inv_le_iff_le_mul'

added theorem mul_inv_le_iff_le_mul

added theorem mul_le_iff_le_one_left'

added theorem mul_le_iff_le_one_right'

added theorem mul_le_mul''

added theorem mul_le_mul'

added theorem mul_le_mul_iff_left

added theorem mul_le_mul_iff_right

added theorem mul_le_mul_left''

added theorem mul_le_mul_left'

added theorem mul_le_mul_right''

added theorem mul_le_mul_right'

added theorem mul_le_mul_three

added theorem mul_le_of_le_inv_mul

added theorem mul_le_of_le_of_le_one'

added theorem mul_le_of_le_of_le_one

added theorem mul_le_of_le_one_of_le'

added theorem mul_le_of_le_one_of_le

added theorem mul_le_one''

added theorem mul_le_one'

added theorem mul_lt_iff_lt_one_left'

added theorem mul_lt_iff_lt_one_right'

added theorem mul_lt_mul'''

added theorem mul_lt_mul_iff_left

added theorem mul_lt_mul_iff_right

added theorem mul_lt_mul_left'

added theorem mul_lt_mul_of_le_of_lt

added theorem mul_lt_mul_of_lt_of_le

added theorem mul_lt_mul_right'

added theorem mul_lt_of_le_of_lt_one

added theorem mul_lt_of_le_one_of_lt'

added theorem mul_lt_of_le_one_of_lt

added theorem mul_lt_of_lt_inv_mul

added theorem mul_lt_of_lt_of_le_one'

added theorem mul_lt_of_lt_of_le_one

added theorem mul_lt_of_lt_of_lt_one'

added theorem mul_lt_of_lt_of_lt_one

added theorem mul_lt_of_lt_one_of_le

added theorem mul_lt_of_lt_one_of_lt'

added theorem mul_lt_of_lt_one_of_lt

added theorem mul_lt_one'

added theorem mul_lt_one

added theorem mul_lt_one_of_le_one_of_lt_one'

added theorem mul_lt_one_of_le_one_of_lt_one

added theorem mul_lt_one_of_lt_one_of_le_one'

added theorem mul_lt_one_of_lt_one_of_le_one

added theorem mul_one_lt'

added theorem mul_one_lt

added theorem mul_one_lt_of_one_le_of_one_lt'

added theorem mul_one_lt_of_one_le_of_one_lt

added theorem mul_one_lt_of_one_lt_of_one_le'

added theorem mul_one_lt_of_one_lt_of_one_le

deleted theorem neg_add_le_iff_le_add'

deleted theorem neg_add_le_iff_le_add

deleted theorem neg_add_le_left_of_le_add

deleted theorem neg_add_le_of_le_add

deleted theorem neg_add_le_right_of_le_add

deleted theorem neg_add_lt_iff_lt_add

deleted theorem neg_add_lt_iff_lt_add_right

deleted theorem neg_add_lt_left_of_lt_add

deleted theorem neg_add_lt_of_lt_add

deleted theorem neg_add_lt_right_of_lt_add

deleted theorem neg_le

deleted theorem neg_le_iff_add_nonneg

deleted theorem neg_le_neg

deleted theorem neg_le_neg_iff

deleted theorem neg_le_of_neg_le

deleted theorem neg_le_self

deleted theorem neg_lt

deleted theorem neg_lt_neg

deleted theorem neg_lt_neg_iff

deleted theorem neg_lt_of_neg_lt

deleted theorem neg_lt_zero

deleted theorem neg_neg_iff_pos

deleted theorem neg_neg_of_pos

deleted theorem neg_nonneg

deleted theorem neg_nonneg_of_nonpos

deleted theorem neg_nonpos

deleted theorem neg_nonpos_of_nonneg

deleted theorem neg_of_neg_pos

deleted theorem neg_pos

deleted theorem neg_pos_of_neg

deleted theorem nonneg_of_neg_nonpos

deleted theorem nonpos_of_neg_nonneg

added theorem one_le_inv'

added theorem one_le_inv_of_le_one

added theorem one_le_mul'

added theorem one_le_mul

added theorem one_le_of_inv_le_one

added theorem one_lt_inv'

added theorem one_lt_inv_of_inv

added theorem one_lt_of_inv_inv

deleted theorem ordered_add_comm_group.add_lt_add_left

deleted theorem ordered_add_comm_group.le_of_add_le_add_left

deleted theorem ordered_add_comm_group.lt_of_add_lt_add_left

deleted def ordered_add_comm_group.mk'

added theorem ordered_comm_group.le_of_mul_le_mul_left

added theorem ordered_comm_group.lt_of_mul_lt_mul_left

added def ordered_comm_group.mk'

added theorem ordered_comm_group.mul_lt_mul_left'

deleted theorem pos_of_neg_neg

added theorem self_le_inv

deleted theorem self_le_neg

deleted theorem strict_mono.add_const

deleted theorem strict_mono.add_monotone

deleted theorem strict_mono.const_add

added theorem strict_mono.const_mul'

added theorem strict_mono.mul_const'

added theorem strict_mono.mul_monotone'

modified theorem units.coe_le_coe

modified theorem units.coe_lt_coe