Commit 2021-06-13 06:04 2c919b08

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.