Lemmas about the interaction of power operations with order in terms of CovariantClass

More lemmas with bundled algebra+order typeclasses are in Algebra/GroupPower/Order.lean and Algebra/GroupPower/Lemmas.lean.

theorem nsmul_le_nsmul_right {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} {b : M} (hab : a ≤ b) (i : ℕ) : i • a ≤ i • b

abbrev nsmul_le_nsmul_right.match_1 (motive : ℕ → Prop) : ∀ (x : ℕ), (Unit → motive 0) → (∀ (k : ℕ), motive (Nat.succ k)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

theorem pow_le_pow_left' {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} {b : M} (hab : a ≤ b) (i : ℕ) : a ^ i ≤ b ^ i

theorem nsmul_nonneg {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} (H : 0 ≤ a) (n : ℕ) : 0 ≤ n • a

theorem one_le_pow_of_one_le' {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} (H : 1 ≤ a) (n : ℕ) : 1 ≤ a ^ n

theorem nsmul_nonpos {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} (H : a ≤ 0) (n : ℕ) : n • a ≤ 0

theorem pow_le_one' {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} (H : a ≤ 1) (n : ℕ) : a ^ n ≤ 1

theorem nsmul_le_nsmul_left {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} {n : ℕ} {m : ℕ} (ha : 0 ≤ a) (h : n ≤ m) : n • a ≤ m • a

abbrev nsmul_le_nsmul_left.match_1 {n : ℕ} {m : ℕ} (motive : (∃ (k : ℕ), n + k = m) → Prop) : ∀ (x : ∃ (k : ℕ), n + k = m), (∀ (k : ℕ) (hk : n + k = m), motive (_ : ∃ (k : ℕ), n + k = m)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

theorem pow_le_pow_right' {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} {n : ℕ} {m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m

theorem nsmul_le_nsmul_left_of_nonpos {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} {n : ℕ} {m : ℕ} (ha : a ≤ 0) (h : n ≤ m) : m • a ≤ n • a

theorem pow_le_pow_right_of_le_one' {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} {n : ℕ} {m : ℕ} (ha : a ≤ 1) (h : n ≤ m) : a ^ m ≤ a ^ n

theorem nsmul_pos {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} (ha : 0 < a) {k : ℕ} (hk : k ≠ 0) : 0 < k • a

theorem one_lt_pow' {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} (ha : 1 < a) {k : ℕ} (hk : k ≠ 0) : 1 < a ^ k

theorem nsmul_neg {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} (ha : a < 0) {k : ℕ} (hk : k ≠ 0) : k • a < 0

theorem pow_lt_one' {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} (ha : a < 1) {k : ℕ} (hk : k ≠ 0) : a ^ k < 1

theorem nsmul_lt_nsmul_left {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {a : M} {n : ℕ} {m : ℕ} (ha : 0 < a) (h : n < m) : n • a < m • a

theorem pow_lt_pow_right' {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] {a : M} {n : ℕ} {m : ℕ} (ha : 1 < a) (h : n < m) : a ^ n < a ^ m

theorem nsmul_left_strictMono {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {a : M} (ha : 0 < a) : StrictMono fun (x : ℕ) => x • a

theorem pow_right_strictMono' {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] {a : M} (ha : 1 < a) : StrictMono fun (x : ℕ) => a ^ x

theorem Left.pow_nonneg {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {x : M} (hx : 0 ≤ x) {n : ℕ} : 0 ≤ n • x

theorem Left.one_le_pow_of_le {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {x : M} (hx : 1 ≤ x) {n : ℕ} : 1 ≤ x ^ n

theorem Left.pow_nonpos {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {x : M} (hx : x ≤ 0) {n : ℕ} : n • x ≤ 0

theorem Left.pow_le_one_of_le {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {x : M} (hx : x ≤ 1) {n : ℕ} : x ^ n ≤ 1

theorem Right.pow_nonneg {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {x : M} (hx : 0 ≤ x) {n : ℕ} : 0 ≤ n • x

theorem Right.one_le_pow_of_le {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {x : M} (hx : 1 ≤ x) {n : ℕ} : 1 ≤ x ^ n

theorem Right.pow_nonpos {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {x : M} (hx : x ≤ 0) {n : ℕ} : n • x ≤ 0

theorem Right.pow_le_one_of_le {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {x : M} (hx : x ≤ 1) {n : ℕ} : x ^ n ≤ 1

abbrev StrictMono.const_nsmul.match_1 (motive : (x : ℕ) → x ≠ 0 → Prop) : ∀ (x : ℕ) (x_1 : x ≠ 0), (∀ (hn : 0 ≠ 0), motive 0 hn) → (∀ (x : 1 ≠ 0), motive 1 x) → (∀ (n : ℕ) (x : Nat.succ (Nat.succ n) ≠ 0), motive (Nat.succ (Nat.succ n)) x) → motive x x_1

Equations

• (_ : motive x✝ x) = (_ : motive x✝ x)

theorem StrictMono.const_nsmul {β : Type u_1} {M : Type u_3} [AddMonoid M] [Preorder M] [Preorder β] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {f : β → M} (hf : StrictMono f) {n : ℕ} : n ≠ 0 → StrictMono fun (x : β) => n • f x

theorem StrictMono.pow_const {β : Type u_1} {M : Type u_3} [Monoid M] [Preorder M] [Preorder β] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] {f : β → M} (hf : StrictMono f) {n : ℕ} : n ≠ 0 → StrictMono fun (x : β) => f x ^ n

theorem nsmul_right_strictMono {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {n : ℕ} (hn : n ≠ 0) : StrictMono fun (x : M) => n • x

theorem pow_left_strictMono {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] {n : ℕ} (hn : n ≠ 0) : StrictMono fun (x : M) => x ^ n

See also pow_left_strictMonoOn.

theorem nsmul_lt_nsmul_right {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {n : ℕ} (hn : n ≠ 0) {a : M} {b : M} (hab : a < b) : n • a < n • b

theorem pow_lt_pow_left' {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] {n : ℕ} (hn : n ≠ 0) {a : M} {b : M} (hab : a < b) : a ^ n < b ^ n

theorem Monotone.const_nsmul {β : Type u_1} {M : Type u_3} [AddMonoid M] [Preorder M] [Preorder β] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {f : β → M} (hf : Monotone f) (n : ℕ) : Monotone fun (a : β) => n • f a

theorem Monotone.pow_const {β : Type u_1} {M : Type u_3} [Monoid M] [Preorder M] [Preorder β] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {f : β → M} (hf : Monotone f) (n : ℕ) : Monotone fun (a : β) => f a ^ n

theorem nsmul_right_mono {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] (n : ℕ) : Monotone fun (a : M) => n • a

theorem pow_left_mono {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] (n : ℕ) : Monotone fun (a : M) => a ^ n

theorem Left.pow_neg {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {n : ℕ} {x : M} (hn : 0 < n) (h : x < 0) : n • x < 0

theorem Left.pow_lt_one_of_lt {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] {n : ℕ} {x : M} (hn : 0 < n) (h : x < 1) : x ^ n < 1

theorem Right.pow_neg {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {n : ℕ} {x : M} (hn : 0 < n) (h : x < 0) : n • x < 0

theorem Right.pow_lt_one_of_lt {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] {n : ℕ} {x : M} (hn : 0 < n) (h : x < 1) : x ^ n < 1

theorem nsmul_nonneg_iff {M : Type u_3} [AddMonoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {x : M} {n : ℕ} (hn : n ≠ 0) : 0 ≤ n • x ↔ 0 ≤ x

theorem one_le_pow_iff {M : Type u_3} [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {x : M} {n : ℕ} (hn : n ≠ 0) : 1 ≤ x ^ n ↔ 1 ≤ x

theorem nsmul_nonpos_iff {M : Type u_3} [AddMonoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {x : M} {n : ℕ} (hn : n ≠ 0) : n • x ≤ 0 ↔ x ≤ 0

theorem pow_le_one_iff {M : Type u_3} [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n ≤ 1 ↔ x ≤ 1

theorem nsmul_pos_iff {M : Type u_3} [AddMonoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {x : M} {n : ℕ} (hn : n ≠ 0) : 0 < n • x ↔ 0 < x

theorem one_lt_pow_iff {M : Type u_3} [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {x : M} {n : ℕ} (hn : n ≠ 0) : 1 < x ^ n ↔ 1 < x

theorem nsmul_neg_iff {M : Type u_3} [AddMonoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {x : M} {n : ℕ} (hn : n ≠ 0) : n • x < 0 ↔ x < 0

theorem pow_lt_one_iff {M : Type u_3} [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n < 1 ↔ x < 1

theorem nsmul_eq_zero_iff {M : Type u_3} [AddMonoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {x : M} {n : ℕ} (hn : n ≠ 0) : n • x = 0 ↔ x = 0

theorem pow_eq_one_iff {M : Type u_3} [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n = 1 ↔ x = 1

theorem nsmul_le_nsmul_iff_left {M : Type u_3} [AddMonoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {a : M} {m : ℕ} {n : ℕ} (ha : 0 < a) : m • a ≤ n • a ↔ m ≤ n

theorem pow_le_pow_iff_right' {M : Type u_3} [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] {a : M} {m : ℕ} {n : ℕ} (ha : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n

theorem nsmul_lt_nsmul_iff_left {M : Type u_3} [AddMonoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {a : M} {m : ℕ} {n : ℕ} (ha : 0 < a) : m • a < n • a ↔ m < n

theorem pow_lt_pow_iff_right' {M : Type u_3} [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] {a : M} {m : ℕ} {n : ℕ} (ha : 1 < a) : a ^ m < a ^ n ↔ m < n

theorem lt_of_nsmul_lt_nsmul_right {M : Type u_3} [AddMonoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} {b : M} (n : ℕ) : n • a < n • b → a < b

theorem lt_of_pow_lt_pow_left' {M : Type u_3} [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} {b : M} (n : ℕ) : a ^ n < b ^ n → a < b

theorem min_lt_of_add_lt_two_nsmul {M : Type u_3} [AddMonoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} {b : M} {c : M} (h : a + b < 2 • c) : min a b < c

theorem min_lt_of_mul_lt_sq {M : Type u_3} [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} {b : M} {c : M} (h : a * b < c ^ 2) : min a b < c

theorem lt_max_of_two_nsmul_lt_add {M : Type u_3} [AddMonoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} {b : M} {c : M} (h : 2 • a < b + c) : a < max b c

theorem lt_max_of_sq_lt_mul {M : Type u_3} [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} {b : M} {c : M} (h : a ^ 2 < b * c) : a < max b c

theorem le_of_nsmul_le_nsmul_right {M : Type u_3} [AddMonoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {a : M} {b : M} {n : ℕ} (hn : n ≠ 0) : n • a ≤ n • b → a ≤ b

theorem le_of_pow_le_pow_left' {M : Type u_3} [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] {a : M} {b : M} {n : ℕ} (hn : n ≠ 0) : a ^ n ≤ b ^ n → a ≤ b

theorem min_le_of_add_le_two_nsmul {M : Type u_3} [AddMonoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {a : M} {b : M} {c : M} (h : a + b ≤ 2 • c) : min a b ≤ c

theorem min_le_of_mul_le_sq {M : Type u_3} [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] {a : M} {b : M} {c : M} (h : a * b ≤ c ^ 2) : min a b ≤ c

theorem le_max_of_two_nsmul_le_add {M : Type u_3} [AddMonoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {a : M} {b : M} {c : M} (h : 2 • a ≤ b + c) : a ≤ max b c

theorem le_max_of_sq_le_mul {M : Type u_3} [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] {a : M} {b : M} {c : M} (h : a ^ 2 ≤ b * c) : a ≤ max b c

theorem Left.nsmul_neg_iff {M : Type u_3} [AddMonoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {n : ℕ} {x : M} (hn : 0 < n) : n • x < 0 ↔ x < 0

theorem Left.pow_lt_one_iff' {M : Type u_3} [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] {n : ℕ} {x : M} (hn : 0 < n) : x ^ n < 1 ↔ x < 1

theorem Left.pow_lt_one_iff {M : Type u_3} [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] {n : ℕ} {x : M} (hn : 0 < n) : x ^ n < 1 ↔ x < 1

theorem Right.nsmul_neg_iff {M : Type u_3} [AddMonoid M] [LinearOrder M] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {n : ℕ} {x : M} (hn : 0 < n) : n • x < 0 ↔ x < 0

theorem Right.pow_lt_one_iff {M : Type u_3} [Monoid M] [LinearOrder M] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] {n : ℕ} {x : M} (hn : 0 < n) : x ^ n < 1 ↔ x < 1

theorem zsmul_nonneg {G : Type u_2} [SubNegMonoid G] [Preorder G] [CovariantClass G G (fun (x x_1 : G) => x + x_1) fun (x x_1 : G) => x ≤ x_1] {x : G} (H : 0 ≤ x) {n : ℤ} (hn : 0 ≤ n) : 0 ≤ n • x

theorem one_le_zpow {G : Type u_2} [DivInvMonoid G] [Preorder G] [CovariantClass G G (fun (x x_1 : G) => x * x_1) fun (x x_1 : G) => x ≤ x_1] {x : G} (H : 1 ≤ x) {n : ℤ} (hn : 0 ≤ n) : 1 ≤ x ^ n

Deprecated lemmas

Those lemmas have been deprecated on 2023-12-23.

@[deprecated pow_le_pow_left']

theorem pow_le_pow_of_le_left' {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} {b : M} (hab : a ≤ b) (i : ℕ) : a ^ i ≤ b ^ i

Alias of pow_le_pow_left'.

@[deprecated nsmul_le_nsmul_right]

theorem nsmul_le_nsmul_of_le_right {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} {b : M} (hab : a ≤ b) (i : ℕ) : i • a ≤ i • b

Alias of nsmul_le_nsmul_right.

@[deprecated pow_lt_pow_right']

theorem pow_lt_pow' {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] {a : M} {n : ℕ} {m : ℕ} (ha : 1 < a) (h : n < m) : a ^ n < a ^ m

Alias of pow_lt_pow_right'.

@[deprecated nsmul_lt_nsmul_left]

theorem nsmul_lt_nsmul {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {a : M} {n : ℕ} {m : ℕ} (ha : 0 < a) (h : n < m) : n • a < m • a

Alias of nsmul_lt_nsmul_left.

@[deprecated pow_right_strictMono']

theorem pow_strictMono_left {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] {a : M} (ha : 1 < a) : StrictMono fun (x : ℕ) => a ^ x

Alias of pow_right_strictMono'.

@[deprecated nsmul_left_strictMono]

theorem nsmul_strictMono_right {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {a : M} (ha : 0 < a) : StrictMono fun (x : ℕ) => x • a

Alias of nsmul_left_strictMono.

@[deprecated StrictMono.pow_const]

theorem StrictMono.pow_right' {β : Type u_1} {M : Type u_3} [Monoid M] [Preorder M] [Preorder β] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] {f : β → M} (hf : StrictMono f) {n : ℕ} : n ≠ 0 → StrictMono fun (x : β) => f x ^ n

Alias of StrictMono.pow_const.

@[deprecated StrictMono.const_nsmul]

theorem StrictMono.nsmul_left {β : Type u_1} {M : Type u_3} [AddMonoid M] [Preorder M] [Preorder β] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {f : β → M} (hf : StrictMono f) {n : ℕ} : n ≠ 0 → StrictMono fun (x : β) => n • f x

Alias of StrictMono.const_nsmul.

@[deprecated pow_left_strictMono]

theorem pow_strictMono_right' {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] {n : ℕ} (hn : n ≠ 0) : StrictMono fun (x : M) => x ^ n

Alias of pow_left_strictMono.

---

See also pow_left_strictMonoOn.

@[deprecated nsmul_right_strictMono]

theorem nsmul_strictMono_left {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {n : ℕ} (hn : n ≠ 0) : StrictMono fun (x : M) => n • x

Alias of nsmul_right_strictMono.

@[deprecated Monotone.pow_const]

theorem Monotone.pow_right {β : Type u_1} {M : Type u_3} [Monoid M] [Preorder M] [Preorder β] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {f : β → M} (hf : Monotone f) (n : ℕ) : Monotone fun (a : β) => f a ^ n

Alias of Monotone.pow_const.

@[deprecated Monotone.const_nsmul]

theorem Monotone.nsmul_left {β : Type u_1} {M : Type u_3} [AddMonoid M] [Preorder M] [Preorder β] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {f : β → M} (hf : Monotone f) (n : ℕ) : Monotone fun (a : β) => n • f a

Alias of Monotone.const_nsmul.

@[deprecated lt_of_pow_lt_pow_left']

theorem lt_of_pow_lt_pow' {M : Type u_3} [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} {b : M} (n : ℕ) : a ^ n < b ^ n → a < b

Alias of lt_of_pow_lt_pow_left'.

@[deprecated lt_of_nsmul_lt_nsmul_right]

theorem lt_of_nsmul_lt_nsmul {M : Type u_3} [AddMonoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} {b : M} (n : ℕ) : n • a < n • b → a < b

Alias of lt_of_nsmul_lt_nsmul_right.

@[deprecated pow_le_pow_right']

theorem pow_le_pow' {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} {n : ℕ} {m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m

Alias of pow_le_pow_right'.

@[deprecated nsmul_le_nsmul_left]

theorem nsmul_le_nsmul {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} {n : ℕ} {m : ℕ} (ha : 0 ≤ a) (h : n ≤ m) : n • a ≤ m • a

Alias of nsmul_le_nsmul_left.

@[deprecated pow_le_pow_right_of_le_one']

theorem pow_le_pow_of_le_one' {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} {n : ℕ} {m : ℕ} (ha : a ≤ 1) (h : n ≤ m) : a ^ m ≤ a ^ n

Alias of pow_le_pow_right_of_le_one'.

@[deprecated nsmul_le_nsmul_left_of_nonpos]

theorem nsmul_le_nsmul_of_nonpos {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {a : M} {n : ℕ} {m : ℕ} (ha : a ≤ 0) (h : n ≤ m) : m • a ≤ n • a

Alias of nsmul_le_nsmul_left_of_nonpos.

@[deprecated le_of_pow_le_pow_left']

theorem le_of_pow_le_pow' {M : Type u_3} [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] {a : M} {b : M} {n : ℕ} (hn : n ≠ 0) : a ^ n ≤ b ^ n → a ≤ b

Alias of le_of_pow_le_pow_left'.

@[deprecated le_of_nsmul_le_nsmul_right]

theorem le_of_nsmul_le_nsmul {M : Type u_3} [AddMonoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {a : M} {b : M} {n : ℕ} (hn : n ≠ 0) : n • a ≤ n • b → a ≤ b

Alias of le_of_nsmul_le_nsmul_right.

@[deprecated pow_le_pow_iff_right']

theorem pow_le_pow_iff' {M : Type u_3} [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] {a : M} {m : ℕ} {n : ℕ} (ha : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n

Alias of pow_le_pow_iff_right'.

@[deprecated nsmul_le_nsmul_iff_left]

theorem nsmul_le_nsmul_iff {M : Type u_3} [AddMonoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {a : M} {m : ℕ} {n : ℕ} (ha : 0 < a) : m • a ≤ n • a ↔ m ≤ n

Alias of nsmul_le_nsmul_iff_left.

@[deprecated pow_lt_pow_iff_right']

theorem pow_lt_pow_iff' {M : Type u_3} [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1] {a : M} {m : ℕ} {n : ℕ} (ha : 1 < a) : a ^ m < a ^ n ↔ m < n

Alias of pow_lt_pow_iff_right'.

@[deprecated nsmul_lt_nsmul_iff_left]

theorem nsmul_lt_nsmul_iff {M : Type u_3} [AddMonoid M] [LinearOrder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {a : M} {m : ℕ} {n : ℕ} (ha : 0 < a) : m • a < n • a ↔ m < n

Alias of nsmul_lt_nsmul_iff_left.

@[deprecated pow_left_mono]

theorem pow_mono_right {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] (n : ℕ) : Monotone fun (a : M) => a ^ n

Alias of pow_left_mono.

@[deprecated nsmul_right_mono]

theorem nsmul_mono_left {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] [CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] (n : ℕ) : Monotone fun (a : M) => n • a

Alias of nsmul_right_mono.