Theorem inv_lt_one₀

Modification history

2024-10-03 10:58

Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

chore: generalise more lemmas from `LinearOrderedField` to `GroupWithZero` (#17359) …

Modified inv_lt_one₀ View on Github →

2024-06-07 11:39

Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

feat(Algebra/Order/GroupWithZero): add `inv_lt_one₀` and `one_lt_inv₀` (#13563) …

Added inv_lt_one₀ View on Github →