Mathlib Map

Theorems · Theorem · order theory

lt_mul_of_one_lt_left

∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [MulPosStrictMono α],
  0 < b → 1 < a → b < a * b
Defined in
Mathlib.Algebra.Order.GroupWithZero.Basic
Cited by
5 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
MulOneClassZeroPreorderMulPosStrictMono
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Seminorm.gauge_ball · cited by 2Seminorm.gauge_balllt_two_mul_self · cited by 2lt_two_mul_selfone_add_mul_self_lt_rpow_one_add · cited by 2one_add_mul_self_lt_rpow_…IsPrimitiveRoot.neZero' · cited by 1IsPrimitiveRoot.neZero'invOf_lt_one · cited by 1invOf_lt_onePreorder · cited by 7952Preorderone_mul · cited by 2841one_mulMulOneClass · cited by 1018MulOneClassMulPosStrictMono · cited by 94MulPosStrictMonomul_lt_mul_of_pos_right · cited by 54mul_lt_mul_of_pos_rightlt_mul_of_one_lt_leftCITED BYCITES

Cites5

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

Cited by5

Results whose statement or proof uses this declaration.