Theorems · Theorem · order theory
inv_lt_zero
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : LinearOrder G₀] {a : G₀} [PosMulMono G₀], a⁻¹ < 0 ↔ a < 0Alias of inv_neg''.
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LinearOrderstatement · cited by 8,572
- GroupWithZerostatement · cited by 691
- PosMulMonostatement · cited by 165
- inv_neg''proof · cited by 7
Cited by6
Results whose statement or proof uses this declaration.
- padicNorm.int_eq_one_iffproof · cited by 3
- EReal.inv_neg_of_neg_ne_botproof · cited by 2
- Hyperreal.infinite_of_infinitesimal_invproof · cited by 1
- Real.tendsto_logb_nhdsNE_zero_of_base_lt_oneproof · cited by 1
- Real.tendsto_logb_nhdsGT_zero_of_base_lt_oneproof · cited by 0
- Real.sign_invproof · cited by 0