Theorems · Theorem · order theory
le_mul_of_one_le_left
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [MulPosMono α],
0 ≤ b → 1 ≤ a → b ≤ a * b- Cited by
- 19 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
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.
- Preorderstatement and proof · cited by 7,952
- one_mulproof · cited by 2,841
- MulOneClassstatement and proof · cited by 1,018
- mul_le_mul_of_nonneg_rightproof · cited by 301
- MulPosMonostatement and proof · cited by 128
Cited by19
Results whose statement or proof uses this declaration.
- Filter.Tendsto.atTop_mul_atTop₀proof · cited by 12
- Cardinal.nat_mul_aleph0proof · cited by 3
- summable_jacobiTheta₂'_term_iffproof · cited by 2
- summable_jacobiTheta₂_term_fderiv_iffproof · cited by 2
- Finset.prod_le_prod_of_subset_of_one_leproof · cited by 2
- round_eq_divproof · cited by 2
- one_lt_mul_of_le_of_ltproof · cited by 2
- NumberField.mixedEmbedding.norm_le_convexBodySumFunproof · cited by 1
- EisensteinSeries.auxbound1proof · cited by 1
- MeasureTheory.L2.eLpNorm_inner_lt_topproof · cited by 1
- invOf_le_oneproof · cited by 1
- VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_leproof · cited by 1