Mathlib Map

Theorems · Theorem · order theory

zsmul_left_mono

∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a : α},
  0 ≤ a → Monotone fun n => n • a
Defined in
Mathlib.Algebra.Order.Group.Basic
Cited by
2 results in Mathlib
Foundations
Depth 34 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AddCommGroupPartialOrderIsOrderedAddMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

zsmul_le_zsmul_left · cited by 2zsmul_le_zsmul_lefttoIcoMod_le_toIocMod · cited by 0toIcoMod_le_toIocModAddCommGroup · cited by 12871AddCommGroupPartialOrder · cited by 6410PartialOrderIsOrderedAddMonoid · cited by 1659IsOrderedAddMonoidMonotone · cited by 1397Monotonele_add_of_nonneg_right · cited by 69le_add_of_nonneg_rightadd_one_zsmul · cited by 19add_one_zsmulmonotone_int_of_le_succ · cited by 3monotone_int_of_le_succzsmul_left_monoCITED BYCITES

Cites7

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.