Theorems · Theorem · order theory

pow_left_strictMono

∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftStrictMono M] [MulRightStrictMono M] {n : ℕ},
  n ≠ 0 → StrictMono fun x => x ^ n

See also pow_left_strictMonoOn₀.

Defined in: Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Cited by: 2 results in Mathlib
Foundations: Depth 13 from the axioms · uses propext, Quot.sound
Assumes: Monoid Preorder MulLeftStrictMono MulRightStrictMono

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites7

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
Monoidstatement and proof · cited by 3,887
StrictMonostatement · cited by 706
MulLeftStrictMonostatement and proof · cited by 146
MulRightStrictMonostatement and proof · cited by 108
strictMono_idproof · cited by 16
StrictMono.pow_constproof · cited by 1

Cited by2

Results whose statement or proof uses this declaration.

pow_le_pow_iff_leftproof · cited by 1
pow_lt_pow_left'proof · cited by 0