Theorems · Theorem · order theory
pos_of_ne_zero
∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : Zero α] [IsBotZeroClass α], a ≠ 0 → 0 < aAlias of the reverse direction of pos_iff_ne_zero.
- Defined in
- Mathlib.Algebra.Order.IsBotOne
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PartialOrderstatement and proof · cited by 6,410
- pos_iff_ne_zeroproof · cited by 180
- IsBotZeroClassstatement and proof · cited by 71
Cited by21
Results whose statement or proof uses this declaration.
- Ne.posproof · cited by 17
- HomogeneousIdeal.irrelevant_eq_iSupproof · cited by 2
- Nat.eq_or_eq_of_totient_eq_totientproof · cited by 2
- AddLECancellable.tsub_lt_self_iffproof · cited by 2
- Module.rank_pos_of_freeproof · cited by 2
- AddSubmonoid.fg_of_subtractiveproof · cited by 2
- dvd_pow_pow_sub_self_of_dvdproof · cited by 2
- Nat.exists_mem_span_nat_finset_of_geproof · cited by 1
- MeasureTheory.IntegrableOn.restrict_toMeasurableproof · cited by 1
- HasCompactSupport.exist_eLpNorm_sub_le_of_continuousproof · cited by 1
- CFC.isUnit_nnrpow_iffproof · cited by 1
- Nat.radical_posproof · cited by 1