Theorem inv_le_one_iff₀

Modification history

2024-10-11 15:01

Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

chore: generalise `zpow` lemmas from `LinearOrderedSemifield` to `GroupWithZero` (#17539)

Modified inv_le_one_iff₀ View on Github →

2024-10-08 18:09

Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

chore: generalise yet more lemmas from `LinearOrderedField` to `GroupWithZero` (#17447)

Added inv_le_one_iff₀ View on Github →