Commit 2021-08-09 13:47 5f2d9548
View on Github →feat(algebra/ordered_field): add inv_le_of_inv_le and inv_lt_of_inv_lt (#8565)
These lemmas need positivity of only one of two variables. Mathlib already had lemmas about ordered multiplicative groups with these names, I appended prime to their names.