Mathlib Map

Theorems · Theorem · order theory

le_mul_self

∀ {α : Type u} [inst : Mul α] [inst_1 : LE α] [CanonicallyOrderedMul α] {a b : α}, a ≤ b * a
Defined in
Mathlib.Algebra.Order.Monoid.Canonical.Defs
Cited by
4 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Assumes
MulLECanonicallyOrderedMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Submonoid.fg_of_divisive · cited by 2Submonoid.fg_of_divisivele_mul_of_le_right · cited by 1le_mul_of_le_rightself_le_mul_left · cited by 0self_le_mul_leftle_of_mul_le_right · cited by 0le_of_mul_le_rightCanonicallyOrderedMul · cited by 51CanonicallyOrderedMulCanonicallyOrderedMul.le_mul_self · cited by 1CanonicallyOrderedMul.le_…le_mul_selfCITED BYCITES

Cites2

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

Cited by4

Results whose statement or proof uses this declaration.