mathlib

2c919b08 - chore(algebra/{ordered_group, linear_ordered_comm_group_with_zero.lean}): rename one lemma, remove more @s (#7895)

chore(algebra/{ordered_group, linear_ordered_comm_group_with_zero.lean}): rename one lemma, remove more @s (#7895) The more substantial part of this PR is changing the name of a lemma from `div_lt_div_iff'` to `mul_inv_lt_mul_inv_iff'`: the lemma proves `a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b`. Furthermore, in the same spirit as a couple of my recent short PRs, I am removing a few more `@`, in order to sweep under the rug, later on, a change in typeclass assumptions. This PR only changes a name, which was used only once, and a few proofs, but no statement. On the path towards PR #7645.