Theorems · Theorem · order theory
mul_le_of_le_one_left
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [MulPosMono α],
0 ≤ b → a ≤ 1 → a * b ≤ b- Cited by
- 37 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 by37
Results whose statement or proof uses this declaration.
- ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_of_le_oneproof · cited by 5
- Wbtw.trans_left_rightproof · cited by 3
- ae_eq_zero_of_integral_contMDiff_smul_eq_zeroproof · cited by 3
- Seminorm.balanced_ball_zeroproof · cited by 3
- summable_dirichletSummandproof · cited by 3
- DirichletCharacter.LSeriesSummable_mulproof · cited by 2
- ZLattice.exists_finsetSum_norm_rpow_le_tsumproof · cited by 2
- PadicInt.norm_mahlerTermproof · cited by 2
- MeasureTheory.exists_continuous_eLpNorm_sub_le_of_closedproof · cited by 2
- mul_lt_one_of_nonneg_of_lt_one_rightproof · cited by 2
- setOfPred_liouvilleWith_subset_auxproof · cited by 2
- DirichletCharacter.summable_neg_log_one_sub_mul_prime_cpowproof · cited by 1