Mathlib Map

Theorems · Theorem · order theory

mul_lt_one_of_nonneg_of_lt_one_right

∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a b : M₀} [MulPosMono M₀],
  a ≤ 1 → 0 ≤ b → b < 1 → a * b < 1
Defined in
Mathlib.Algebra.Order.GroupWithZero.Basic
Cited by
2 results in Mathlib
Foundations
Depth 7 from the axioms · uses no axioms
Assumes
MonoidWithZeroPreorderMulPosMono
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Wbtw.trans_left_right · cited by 3Wbtw.trans_left_rightPadicInt.norm_lt_one_mul · cited by 0PadicInt.norm_lt_one_mulPreorder · cited by 7952PreorderLE.le.trans_lt · cited by 795le.trans_ltMonoidWithZero · cited by 456MonoidWithZeroMulPosMono · cited by 128MulPosMonomul_le_of_le_one_left · cited by 37mul_le_of_le_one_leftmul_lt_one_of_nonneg_of_lt_on…CITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.