Commit 2022-12-06 13:59 439961d9

View on Github →

feat: port algebra.order.group.defs (#869) Tracking mathlib commit: f1a2caaf51ef593799107fe9a8d5e411599f3996

Estimated changes

deleted theorem Left.one_lt_inv_iff
deleted theorem one_lt_div'
added structure AddCommGroup.PositiveCone
added theorem Antitone.inv
added theorem AntitoneOn.inv
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 Monotone.inv
added theorem MonotoneOn.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
added theorem StrictAnti.inv
added theorem StrictAntiOn.inv
added theorem StrictMono.inv
added theorem StrictMonoOn.inv
added theorem cmp_div_one'
added theorem div_le_comm
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_le_self_iff
added theorem div_lt_comm
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'
added theorem div_lt_self_iff
added theorem eq_one_of_inv_eq'
added theorem exists_one_lt'
added theorem inv_le_div_iff_le_mul'
added theorem inv_le_div_iff_le_mul
added theorem inv_le_iff_one_le_mul'
added theorem inv_le_iff_one_le_mul
added theorem inv_le_inv'
added theorem inv_le_inv_iff
added theorem inv_le_one_of_one_le
added theorem inv_lt'
added theorem inv_lt_div_iff_lt_mul'
added theorem inv_lt_div_iff_lt_mul
added theorem inv_lt_iff_one_lt_mul'
added theorem inv_lt_iff_one_lt_mul
added theorem inv_lt_inv'
added theorem inv_lt_inv_iff
added theorem inv_lt_one_of_one_lt
added theorem inv_mul_le_iff_le_mul'
added theorem inv_mul_le_iff_le_mul
added theorem inv_mul_le_one_iff
added theorem inv_mul_lt_iff_lt_mul'
added theorem inv_mul_lt_iff_lt_mul
added theorem inv_mul_lt_one_iff
added theorem inv_mul_lt_one_iff_lt
added theorem le_div_comm
added theorem le_div_iff_mul_le'
added theorem le_div_iff_mul_le
added theorem le_div_self_iff
added theorem le_inv_mul_iff_le
added theorem le_inv_mul_iff_mul_le
added theorem le_mul_inv_iff_le
added theorem le_mul_inv_iff_mul_le
added theorem lt_div_comm
added theorem lt_div_iff_mul_lt'
added theorem lt_div_iff_mul_lt
added theorem lt_inv'
added theorem lt_inv_iff_mul_lt_one'
added theorem lt_inv_iff_mul_lt_one
added theorem lt_inv_mul_iff_lt
added theorem lt_inv_mul_iff_mul_lt
added theorem lt_mul_inv_iff_lt
added theorem lt_mul_inv_iff_mul_lt
added theorem mul_inv_le_iff_le_mul'
added 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_one_iff
added theorem one_le_div'
added theorem one_le_inv_of_le_one
added theorem one_lt_div'
deleted theorem neg_neg_of_pos
deleted theorem neg_nonpos_of_nonneg
deleted theorem sub_neg_of_lt
deleted theorem sub_nonpos_of_le