Commit 2021-03-03 13:41 3c9399d1

chore(algebra/ordered_group): put to_additive on lemmas about linear_ordered_comm_group (#6506) No lemmas are added or renamed for the additive version, this just adds lemmas (and more importantly instances) for the multiplicative version. This:

• Adds missing ancestor attributes to linear_ordered_add_comm_group and linear_ordered_comm_group, which are needed to make to_additive work correctly on to_add_comm_group and to_comm_group
• Adds multiplicative versions of:
  • sub_le_self_iff (div_le_self_iff)
  • sub_lt_self_iff (div_lt_self_iff )
  • linear_ordered_add_comm_group.to_linear_ordered_cancel_add_comm_monoid (linear_ordered_comm_group.to_linear_ordered_cancel_comm_monoid)
  • linear_ordered_add_comm_group.add_lt_add_left (linear_ordered_comm_group.mul_lt_mul_left')
  • min_neg_neg (min_inv_inv')
  • max_neg_neg (max_inv_inv')
  • min_sub_sub_right (min_div_div_right')
  • min_sub_sub_left (min_div_div_left')
  • max_sub_sub_right (max_div_div_right')
  • max_sub_sub_left (max_div_div_left')
  • max_zero_sub_eq_self (max_one_div_eq_self')
  • eq_zero_of_neg_eq (eq_one_of_inv_eq')
  • exists_zero_lt (exists_one_lt')