Theorem one_lt_inv₀

Modification history

2024-10-03 10:58

Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

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

Modified one_lt_inv₀ 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 one_lt_inv₀ View on Github →