Theorems · Theorem · order theory
le_zero_iff
∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : Zero α] [IsBotZeroClass α], a ≤ 0 ↔ a = 0Alias of nonpos_iff_eq_zero.
- Defined in
- Mathlib.Algebra.Order.IsBotOne
- Cited by
- 15 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 · cited by 6,410
- nonpos_iff_eq_zeroproof · cited by 100
- IsBotZeroClassstatement · cited by 71
Cited by15
Results whose statement or proof uses this declaration.
- Valuation.Integers.dvd_of_leproof · cited by 4
- LieAlgebra.derivedSeriesOfIdeal_leproof · cited by 4
- exists_finset_linearIndependent_of_le_finrankproof · cited by 2
- MeasureTheory.VectorMeasure.variation_apply_eq_zeroproof · cited by 1
- ruzsaSzemerediNumberNat_oneproof · cited by 1
- ruzsaSzemerediNumberNat_twoproof · cited by 1
- ruzsaSzemerediNumberNat_zeroproof · cited by 1
- MeasureTheory.Measure.exists_positive_of_not_mutuallySingularproof · cited by 1
- AddGroup.rank_eq_zeroproof · cited by 1
- alternatingGroup.mem_kleinFour_of_order_two_powproof · cited by 1
- IsDedekindDomain.HeightOneSpectrum.exists_intValuation_mul_sub_ltproof · cited by 1
- Group.rank_eq_zeroproof · cited by 1