mathlib

462b9509 - chore(algebra/order/field): fill in missing lemma (#14111)

chore(algebra/order/field): fill in missing lemma (#14111) We had `inv_le_inv` and its backward direction, this fills in the backward direction for `inv_lt_inv`. Co-authored-by: Bhavik Mehta <bm489@cam.ac.uk>