Commit 2024-07-16 22:43 126510dd

View on Github →

chore (Algebra.Order.Ring.Defs): split file and unbundle results (#14393) All of the theorems in Algebra.Order.Ring.Defs currently take bundled ordered algebraic typeclasses, eg OrderedSemiring as paramaters unecessarily. We unbundle the results keeping the algebra and order data/theorems separate and adding the mixin compatbility typeclasses as needed and place the theorems in Algebra.Order.Ring.Unbundled.Basic. As Algebra.Order.Ring.Defs and upstream resuls already allow us to pass from bundled classes to unbundled classes appropriately, we lose no uusability by doing this. We lessen dependecies and gain future flexibility.

Estimated changes

deleted theorem Antitone.const_mul
deleted theorem Antitone.mul
deleted theorem Antitone.mul_const
deleted theorem Antitone.mul_monotone
deleted theorem Monotone.const_mul
deleted theorem Monotone.mul
deleted theorem Monotone.mul_antitone
deleted theorem Monotone.mul_const
deleted theorem Monotone.mul_strictMono
deleted theorem StrictAnti.const_mul
deleted theorem StrictAnti.mul_const
deleted theorem StrictMono.const_mul
deleted theorem StrictMono.mul
deleted theorem StrictMono.mul_const
deleted theorem StrictMono.mul_monotone
deleted theorem Units.inv_neg
deleted theorem Units.inv_pos
deleted theorem add_le_mul'
deleted theorem add_le_mul
deleted theorem add_le_mul_two_add
deleted theorem add_one_le_two_mul
deleted theorem antitone_mul_left
deleted theorem antitone_mul_right
deleted theorem cmp_mul_neg_left
deleted theorem cmp_mul_neg_right
deleted theorem cmp_mul_pos_left
deleted theorem cmp_mul_pos_right
deleted theorem le_iff_exists_nonneg_add
deleted theorem le_mul_of_le_one_left
deleted theorem le_mul_of_le_one_right
deleted theorem le_of_mul_le_of_one_le
deleted theorem lt_mul_left
deleted theorem lt_mul_of_lt_one_left
deleted theorem lt_mul_of_lt_one_right
deleted theorem lt_mul_right
deleted theorem lt_mul_self
deleted theorem lt_two_mul_self
deleted theorem max_mul_of_nonneg
deleted theorem min_mul_of_nonneg
deleted theorem mul_le_mul_left_of_neg
deleted theorem mul_le_mul_of_nonpos_left
deleted theorem mul_le_mul_right_of_neg
deleted theorem mul_le_of_one_le_left
deleted theorem mul_le_of_one_le_right
deleted theorem mul_le_one
deleted theorem mul_lt_mul''
deleted theorem mul_lt_mul'
deleted theorem mul_lt_mul
deleted theorem mul_lt_mul_left_of_neg
deleted theorem mul_lt_mul_of_neg_left
deleted theorem mul_lt_mul_of_neg_right
deleted theorem mul_lt_mul_right_of_neg
deleted theorem mul_lt_of_one_lt_left
deleted theorem mul_lt_of_one_lt_right
deleted theorem mul_max_of_nonneg
deleted theorem mul_min_of_nonneg
deleted theorem mul_neg_iff
deleted theorem mul_nonneg_iff
deleted theorem mul_nonneg_of_three
deleted theorem mul_nonpos_iff
deleted theorem mul_pos_iff
deleted theorem mul_pos_of_neg_of_neg
deleted theorem mul_self_inj
deleted theorem mul_self_le_mul_self_iff
deleted theorem mul_self_lt_mul_self
deleted theorem mul_self_lt_mul_self_iff
deleted theorem mul_self_nonneg
deleted theorem mul_self_pos
deleted theorem neg_iff_pos_of_mul_neg
deleted theorem neg_of_mul_neg_left
deleted theorem neg_of_mul_neg_right
deleted theorem neg_one_lt_zero
deleted theorem nonneg_of_mul_nonneg_left
deleted theorem nonneg_of_mul_nonpos_left
deleted theorem nonpos_of_mul_nonneg_left
deleted theorem nonpos_of_mul_nonpos_left
deleted theorem one_lt_mul_of_le_of_lt
deleted theorem one_lt_mul_of_lt_of_le
deleted theorem pos_iff_neg_of_mul_neg
deleted theorem pos_of_mul_neg_left
deleted theorem pos_of_mul_neg_right
deleted theorem pow_le_of_le_one
deleted theorem pow_le_pow_of_le_one
deleted theorem pow_nonneg
deleted theorem pow_pos
deleted theorem sq_le
deleted theorem sq_nonneg
deleted theorem strictAnti_mul_left
deleted theorem strictAnti_mul_right
deleted theorem strictMonoOn_mul_self
deleted theorem sub_one_lt
deleted theorem two_mul_le_add_sq
added theorem Antitone.const_mul
added theorem Antitone.mul
added theorem Antitone.mul_const
added theorem Antitone.mul_monotone
added theorem Monotone.const_mul
added theorem Monotone.mul
added theorem Monotone.mul_antitone
added theorem Monotone.mul_const
added theorem StrictAnti.const_mul
added theorem StrictAnti.mul_const
added theorem StrictMono.const_mul
added theorem StrictMono.mul
added theorem StrictMono.mul_const
added theorem Units.inv_neg
added theorem Units.inv_pos
added theorem add_le_mul'
added theorem add_le_mul
added theorem add_le_mul_two_add
added theorem add_one_le_two_mul
added theorem antitone_mul_left
added theorem antitone_mul_right
added theorem cmp_mul_neg_left
added theorem cmp_mul_neg_right
added theorem cmp_mul_pos_left
added theorem cmp_mul_pos_right
added theorem le_mul_of_le_one_left
added theorem le_mul_of_le_one_right
added theorem le_of_mul_le_of_one_le
added theorem lt_mul_left
added theorem lt_mul_of_lt_one_left
added theorem lt_mul_of_lt_one_right
added theorem lt_mul_right
added theorem lt_mul_self
added theorem lt_two_mul_self
added theorem max_mul_of_nonneg
added theorem min_mul_of_nonneg
added theorem mul_le_mul_left_of_neg
added theorem mul_le_of_one_le_left
added theorem mul_le_of_one_le_right
added theorem mul_le_one
added theorem mul_lt_mul''
added theorem mul_lt_mul'
added theorem mul_lt_mul
added theorem mul_lt_mul_left_of_neg
added theorem mul_lt_mul_of_neg_left
added theorem mul_lt_of_one_lt_left
added theorem mul_lt_of_one_lt_right
added theorem mul_max_of_nonneg
added theorem mul_min_of_nonneg
added theorem mul_neg_iff
added theorem mul_nonneg_iff
added theorem mul_nonneg_of_three
added theorem mul_nonpos_iff
added theorem mul_pos_iff
added theorem mul_pos_of_neg_of_neg
added theorem mul_self_inj
added theorem mul_self_lt_mul_self
added theorem mul_self_nonneg
added theorem mul_self_pos
added theorem neg_iff_pos_of_mul_neg
added theorem neg_of_mul_neg_left
added theorem neg_of_mul_neg_right
added theorem neg_one_lt_zero
added theorem one_lt_mul_of_le_of_lt
added theorem one_lt_mul_of_lt_of_le
added theorem pos_iff_neg_of_mul_neg
added theorem pos_of_mul_neg_left
added theorem pos_of_mul_neg_right
added theorem pow_le_of_le_one
added theorem pow_le_pow_of_le_one
added theorem pow_nonneg
added theorem pow_pos
added theorem sq_le
added theorem sq_nonneg
added theorem strictAnti_mul_left
added theorem strictAnti_mul_right
added theorem strictMonoOn_mul_self
added theorem sub_one_lt
added theorem two_mul_le_add_sq