Theorems · Theorem · order theory
inv_nonpos
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : LinearOrder G₀] {a : G₀} [PosMulMono G₀], a⁻¹ ≤ 0 ↔ a ≤ 0- Cited by
- 9 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LinearOrderstatement and proof · cited by 8,572
- GroupWithZerostatement and proof · cited by 691
- PosMulReflectLTproof · cited by 278
- PosMulMonostatement and proof · cited by 165
- PosMulMono.toPosMulReflectLTproof · cited by 5
Cited by9
Results whose statement or proof uses this declaration.
- div_nonpos_of_nonneg_of_nonposproof · cited by 6
- Real.toNNReal_invproof · cited by 5
- Int.log_of_right_le_zeroproof · cited by 3
- AkraBazziRecurrence.GrowsPolynomially.invproof · cited by 3
- Int.clog_of_right_le_zeroproof · cited by 3
- Rat.toNNRat_invproof · cited by 2
- Int.clog_invproof · cited by 2
- one_div_nonposproof · cited by 1
- EReal.inv_nonpos_of_nonposproof · cited by 1