Theorems · Theorem · order theory
Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg
∀ {α : Type u_4} [inst : GroupWithZero α] [inst_1 : PartialOrder α] {a b : α} [PosMulReflectLT α],
0 < a → 0 ≤ b → 0 ≤ a / b- Defined in
- Mathlib.Algebra.Order.Field.Basic
- Cited by
- 29 results in Mathlib
- Foundations
- Depth 23 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
- LT.lt.leproof · cited by 2,189
- GroupWithZerostatement and proof · cited by 691
- PosMulReflectLTstatement and proof · cited by 278
- div_nonnegproof · cited by 103
Cited by29
Results whose statement or proof uses this declaration.
- PeriodPair.summable_weierstrassPExceptSummandproof · cited by 3
- MeasureTheory.eLpNorm'_mono_enorm_aeproof · cited by 3
- MeasureTheory.memLp_const_enormproof · cited by 3
- not_summable_one_div_on_primesproof · cited by 2
- MeasureTheory.norm_indicatorConstLp_leproof · cited by 2
- MeasureTheory.pow_mul_meas_ge_le_eLpNormproof · cited by 2
- LSeries.tendsto_cpow_mul_atTopproof · cited by 2
- MeasureTheory.tilted_tiltedproof · cited by 2
- Chebyshev.integral_theta_div_log_sq_isBigOproof · cited by 2
- MeasureTheory.toReal_rnDeriv_tilted_leftproof · cited by 1
- RingSeminorm.exists_index_pow_leproof · cited by 1
- MeasureTheory.MemLp.eLpNorm_indicator_norm_ge_leproof · cited by 1