Mathlib v3 is deprecated. Go to Mathlib v4

Theorem inv_neg

Modification history

2020-05-02 12:33

src/algebra/field.lean

chore(algebra/ordered_field): move inv_neg to field and prove for division ring (#2588) …

Modified inv_neg View on Github →

2018-01-14 21:59

algebra/field.lean

feat(algebra/field): more division lemmas

Modified inv_neg View on Github →

2017-08-10 16:36

algebra/field.lean

construct reals as complete, linear ordered field

Added inv_neg View on Github →