Commit 2024-07-31 01:56 59d41574

View on Github →

chore (Algebra.Order.Ring.Unbundled.Basic): inline typeclass assumptions (#15334) We improve the generality of the results here by using inlined typeclass assumptions. It also makes this file comport better with the new variable inclusion mechanism. See Zulip.

Estimated changes

modified theorem Antitone.const_mul
modified theorem Antitone.mul
modified theorem Antitone.mul_const
modified theorem Antitone.mul_monotone
modified theorem Monotone.const_mul
modified theorem Monotone.mul
modified theorem Monotone.mul_antitone
modified theorem Monotone.mul_const
modified theorem Monotone.mul_strictMono
modified theorem StrictAnti.const_mul
modified theorem StrictAnti.const_mul_of_neg
modified theorem StrictAnti.mul_const
modified theorem StrictAnti.mul_const_of_neg
modified theorem StrictMono.const_mul
modified theorem StrictMono.const_mul_of_neg
modified theorem StrictMono.mul
modified theorem StrictMono.mul_const
modified theorem StrictMono.mul_const_of_neg
modified theorem StrictMono.mul_monotone
modified theorem Units.inv_neg
modified theorem Units.inv_pos
modified theorem add_le_mul'
modified theorem add_le_mul
modified theorem add_le_mul_of_left_le_right
modified theorem add_le_mul_of_right_le_left
modified theorem add_le_mul_two_add
modified theorem antitone_mul_left
modified theorem antitone_mul_right
modified theorem cmp_mul_neg_left
modified theorem cmp_mul_neg_right
modified theorem cmp_mul_pos_left
modified theorem cmp_mul_pos_right
modified theorem le_iff_exists_nonneg_add
modified theorem le_mul_of_le_one_left
modified theorem le_mul_of_le_one_right
modified theorem le_of_mul_le_of_one_le
modified theorem lt_mul_left
modified theorem lt_mul_of_lt_one_left
modified theorem lt_mul_of_lt_one_right
modified theorem lt_mul_right
modified theorem lt_mul_self
modified theorem lt_two_mul_self
modified theorem max_mul_of_nonneg
modified theorem min_mul_of_nonneg
modified theorem monotone_mul_left_of_nonneg
modified theorem mul_add_mul_le_mul_add_mul'
modified theorem mul_add_mul_le_mul_add_mul
modified theorem mul_add_mul_lt_mul_add_mul'
modified theorem mul_add_mul_lt_mul_add_mul
modified theorem mul_le_mul_left_of_neg
modified theorem mul_le_mul_of_nonpos_left
modified theorem mul_le_mul_of_nonpos_right
modified theorem mul_le_mul_right_of_neg
modified theorem mul_le_of_one_le_left
modified theorem mul_le_of_one_le_right
modified theorem mul_le_one
modified theorem mul_lt_mul_left_of_neg
modified theorem mul_lt_mul_of_neg_left
modified theorem mul_lt_mul_of_neg_right
modified theorem mul_lt_mul_right_of_neg
modified theorem mul_lt_of_one_lt_left
modified theorem mul_lt_of_one_lt_right
modified theorem mul_max_of_nonneg
modified theorem mul_min_of_nonneg
modified theorem mul_neg_iff
modified theorem mul_nonneg_iff
modified theorem mul_nonneg_iff_of_pos_left
modified theorem mul_nonneg_iff_of_pos_right
modified theorem mul_nonneg_of_three
modified theorem mul_nonpos_iff
modified theorem mul_pos_iff
modified theorem mul_pos_of_neg_of_neg
modified theorem mul_self_inj
modified theorem mul_self_le_mul_self_iff
modified theorem mul_self_lt_mul_self
modified theorem mul_self_lt_mul_self_iff
modified theorem mul_self_nonneg
modified theorem mul_self_pos
modified theorem neg_iff_pos_of_mul_neg
modified theorem neg_one_lt_zero
modified theorem nonneg_of_mul_nonneg_left
modified theorem nonneg_of_mul_nonneg_right
modified theorem nonneg_of_mul_nonpos_left
modified theorem nonneg_of_mul_nonpos_right
modified theorem nonpos_of_mul_nonneg_left
modified theorem nonpos_of_mul_nonneg_right
modified theorem nonpos_of_mul_nonpos_left
modified theorem nonpos_of_mul_nonpos_right
modified theorem one_lt_mul_of_le_of_lt
modified theorem one_lt_mul_of_lt_of_le
modified theorem pos_iff_neg_of_mul_neg
modified theorem pos_of_mul_neg_left
modified theorem pos_of_mul_neg_right
modified theorem pow_le_of_le_one
modified theorem pow_le_pow_of_le_one
modified theorem pow_nonneg
modified theorem pow_pos
modified theorem sq_le
modified theorem sq_nonneg
modified theorem strictAnti_mul_left
modified theorem strictAnti_mul_right
modified theorem strictMonoOn_mul_self
modified theorem strictMono_mul_left_of_pos
modified theorem strictMono_mul_right_of_pos
modified theorem sub_one_lt
modified theorem two_mul_le_add_sq