Commit 2020-05-02 12:33 1cc83e9c
View on Github →chore(algebra/ordered_field): move inv_neg to field and prove for division ring (#2588)
neg_inv this lemma with the equality swapped was already in the library, so maybe we should just get rid of this or neg_inv
Zulip thread