Theorems · Theorem · order theory
one_div_nonneg
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀}, 0 ≤ 1 / a ↔ 0 ≤ a- Cited by
- 11 results in Mathlib
- Foundations
- Depth 22 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.
- PartialOrderstatement and proof · cited by 6,410
- GroupWithZerostatement and proof · cited by 691
- one_divproof · cited by 624
- PosMulReflectLTstatement and proof · cited by 278
- inv_nonnegproof · cited by 56
Cited by11
Results whose statement or proof uses this declaration.
- Nat.one_div_cast_nonnegproof · cited by 2
- summable_one_div_pow_of_leproof · cited by 2
- Real.harm_mean_le_geom_mean_weightedproof · cited by 1
- MeasureTheory.UniformIntegrable.spec'proof · cited by 1
- Real.cos_lt_one_div_sqrt_sq_add_oneproof · cited by 1
- tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_supportproof · cited by 1
- spectrum.limsup_pow_nnnorm_pow_one_div_le_spectralRadiusproof · cited by 1
- Real.Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gammaproof · cited by 1
- norm_midpoint_lt_iffproof · cited by 0
- spectralValue_le_one_iffproof · cited by 0
- div_mul_le_div_mul_of_div_le_divproof · cited by 0