Theorems · Theorem · order theory
inv_lt_inv_iff
∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a b : α} [MulRightStrictMono α],
a⁻¹ < b⁻¹ ↔ b < a- Cited by
- 9 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Groupstatement and proof · cited by 6,238
- one_mulproof · cited by 2,841
- MulLeftStrictMonostatement and proof · cited by 146
- mul_inv_cancelproof · cited by 128
- MulRightStrictMonostatement and proof · cited by 108
- inv_mul_cancel_rightproof · cited by 70
- mul_lt_mul_iff_rightproof · cited by 18
- mul_lt_mul_iff_leftproof · cited by 14
Cited by9
Results whose statement or proof uses this declaration.
- inv_lt'proof · cited by 6
- lt_inv'proof · cited by 4
- div_lt_div_iff_leftproof · cited by 1
- inv_lt_inv'proof · cited by 1
- StrictMonoOn.invproof · cited by 0
- lt_of_inv_lt_invproof · cited by 0
- StrictMono.invproof · cited by 0
- StrictAnti.invproof · cited by 0
- StrictAntiOn.invproof · cited by 0