mathlib

e35a703f - feat(algebra/ordered_{group,field}): more lemmas relating inv and mul inequalities (#5561)

feat(algebra/ordered_{group,field}): more lemmas relating inv and mul inequalities (#5561) I also renamed `inv_le_iff_one_le_mul` to `inv_le_iff_one_le_mul'` for consistency with `div_le_iff` and `div_le_iff'` (unprimed lemmas involve multiplication on the right and primed lemmas involve multiplication on the left).