Theorem inv_neg_one

Modification history

2025-01-07 20:33

Mathlib/Algebra/Field/Basic.lean

chore: move results about `DivisionMonoid` + `HasDistribNeg` (#20551) …

Modified inv_neg_one View on Github →

2023-01-27 15:48

Mathlib/Algebra/Field/Basic.lean

feat: `Rat` functionality for `ring` (#1711) …

Added inv_neg_one View on Github →