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

theorem nsmul_le_nsmul_right {M : Type u_3} [] [] [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 : ) :
∀ (x : ), (Unitmotive 0)(∀ (k : ), motive k.succ)motive x
Equations
• =
Instances For
theorem pow_le_pow_left' {M : Type u_3} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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 )motive x
Equations
• =
Instances For
theorem pow_le_pow_right' {M : Type u_3} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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 0Prop) :
∀ (x : ) (x_1 : x 0), (∀ (hn : 0 0), motive 0 hn)(∀ (x : 1 0), motive 1 x)(∀ (n : ) (x : n.succ.succ 0), motive n.succ.succ x)motive x x_1
Equations
• =
Instances For
theorem StrictMono.const_nsmul {β : Type u_1} {M : Type u_3} [] [] [] [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 : ) {n : } :
n 0StrictMono fun (x : β) => n f x
theorem StrictMono.pow_const {β : Type u_1} {M : Type u_3} [] [] [] [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 : ) {n : } :
n 0StrictMono fun (x : β) => f x ^ n
theorem nsmul_right_strictMono {M : Type u_3} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [] [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 : ) (n : ) :
Monotone fun (a : β) => n f a
theorem Monotone.pow_const {β : Type u_1} {M : Type u_3} [] [] [] [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 : ) (n : ) :
Monotone fun (a : β) => f a ^ n
theorem nsmul_right_mono {M : Type u_3} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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 ba < b
theorem lt_of_pow_lt_pow_left' {M : Type u_3} [] [] [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 ^ na < b
theorem min_lt_of_add_lt_two_nsmul {M : Type u_3} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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 ba b
theorem le_of_pow_le_pow_left' {M : Type u_3} [] [] [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 ^ na b
theorem min_le_of_add_le_two_nsmul {M : Type u_3} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [] [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 : ) {n : } :
n 0StrictMono 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} [] [] [] [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 : ) {n : } :
n 0StrictMono fun (x : β) => n f x

Alias of StrictMono.const_nsmul.

@[deprecated pow_left_strictMono]
theorem pow_strictMono_right' {M : Type u_3} [] [] [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} [] [] [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} [] [] [] [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 : ) (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} [] [] [] [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 : ) (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} [] [] [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 ^ na < 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} [] [] [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 ba < b

Alias of lt_of_nsmul_lt_nsmul_right.

@[deprecated pow_le_pow_right']
theorem pow_le_pow' {M : Type u_3} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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 ^ na 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} [] [] [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 ba b

Alias of le_of_nsmul_le_nsmul_right.

@[deprecated pow_le_pow_iff_right']
theorem pow_le_pow_iff' {M : Type u_3} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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.