mathlib

3c9399d1 - chore(algebra/ordered_group): put to_additive on lemmas about linear_ordered_comm_group (#6506)

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'`)