Documentation

Mathlib.Algebra.Order.Monoid.Unbundled.Pow

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

source
theorem Left.one_le_pow_of_le {M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} (ha : 1 ≤ a) (n : ℕ) :
1 ≤ a ^ n
source
theorem Left.nsmul_nonneg {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftMono M] {a : M} (ha : 0 ≤ a) (n : ℕ) :
0 ≤ n • a
source
theorem Left.pow_le_one_of_le {M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} (ha : a ≤ 1) (n : ℕ) :
a ^ n ≤ 1
source
theorem Left.nsmul_nonpos {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftMono M] {a : M} (ha : a ≤ 0) (n : ℕ) :
n • a ≤ 0
source
theorem Left.pow_lt_one_of_lt {M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} {n : ℕ} (h : a < 1) (hn : n ≠ 0) :
a ^ n < 1
source
theorem Left.nsmul_neg {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftMono M] {a : M} {n : ℕ} (h : a < 0) (hn : n ≠ 0) :
n • a < 0
source
theorem one_le_pow_of_one_le' {M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} (ha : 1 ≤ a) (n : ℕ) :
1 ≤ a ^ n

Alias of Left.one_le_pow_of_le.

source
theorem nsmul_nonneg {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftMono M] {a : M} (ha : 0 ≤ a) (n : ℕ) :
0 ≤ n • a

Alias of Left.nsmul_nonneg.

source
theorem pow_le_one' {M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} (ha : a ≤ 1) (n : ℕ) :
a ^ n ≤ 1

Alias of Left.pow_le_one_of_le.

source
theorem nsmul_nonpos {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftMono M] {a : M} (ha : a ≤ 0) (n : ℕ) :
n • a ≤ 0

Alias of Left.nsmul_nonpos.

source
theorem pow_lt_one' {M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} {n : ℕ} (h : a < 1) (hn : n ≠ 0) :
a ^ n < 1

Alias of Left.pow_lt_one_of_lt.

source
theorem nsmul_neg {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftMono M] {a : M} {n : ℕ} (h : a < 0) (hn : n ≠ 0) :
n • a < 0

Alias of Left.nsmul_neg.

source
theorem pow_right_monotone {M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} (ha : 1 ≤ a) :
Monotone fun (n : ℕ) => a ^ n
source
theorem nsmul_left_monotone {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftMono M] {a : M} (ha : 0 ≤ a) :
Monotone fun (n : ℕ) => n • a
source
theorem pow_le_pow_right' {M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} {n m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) :
a ^ n ≤ a ^ m
source
theorem nsmul_le_nsmul_left {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftMono M] {a : M} {n m : ℕ} (ha : 0 ≤ a) (h : n ≤ m) :
n • a ≤ m • a
source
theorem pow_le_pow_right_of_le_one' {M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} {n m : ℕ} (ha : a ≤ 1) (h : n ≤ m) :
a ^ m ≤ a ^ n
source
theorem nsmul_le_nsmul_left_of_nonpos {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftMono M] {a : M} {n m : ℕ} (ha : a ≤ 0) (h : n ≤ m) :
m • a ≤ n • a
source
theorem one_lt_pow' {M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} (ha : 1 < a) {k : ℕ} (hk : k ≠ 0) :
1 < a ^ k
source
theorem nsmul_pos {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftMono M] {a : M} (ha : 0 < a) {k : ℕ} (hk : k ≠ 0) :
0 < k • a
source
theorem le_self_pow {M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {a : M} {n : ℕ} (ha : 1 ≤ a) (hn : n ≠ 0) :
a ≤ a ^ n
source
theorem le_self_nsmul {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftMono M] {a : M} {n : ℕ} (ha : 0 ≤ a) (hn : n ≠ 0) :
a ≤ n • a
source
theorem pow_right_strictMono' {M : Type u_3} [Monoid M] [Preorder M] [MulLeftStrictMono M] {a : M} (ha : 1 < a) :
StrictMono fun (x : ℕ) => a ^ x
source
theorem nsmul_left_strictMono {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] {a : M} (ha : 0 < a) :
StrictMono fun (x : ℕ) => x • a
source
theorem pow_lt_pow_right' {M : Type u_3} [Monoid M] [Preorder M] [MulLeftStrictMono M] {a : M} {n m : ℕ} (ha : 1 < a) (h : n < m) :
a ^ n < a ^ m
source
theorem nsmul_lt_nsmul_left {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] {a : M} {n m : ℕ} (ha : 0 < a) (h : n < m) :
n • a < m • a
source
theorem Right.one_le_pow_of_le {M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] {x : M} (hx : 1 ≤ x) {n : ℕ} :
1 ≤ x ^ n
source
theorem Right.nsmul_nonneg {M : Type u_3} [AddMonoid M] [Preorder M] [AddRightMono M] {x : M} (hx : 0 ≤ x) {n : ℕ} :
0 ≤ n • x
source
theorem Right.pow_le_one_of_le {M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] {x : M} (hx : x ≤ 1) {n : ℕ} :
x ^ n ≤ 1
source
theorem Right.nsmul_nonpos {M : Type u_3} [AddMonoid M] [Preorder M] [AddRightMono M] {x : M} (hx : x ≤ 0) {n : ℕ} :
n • x ≤ 0
source
theorem Right.pow_lt_one_of_lt {M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] {n : ℕ} {x : M} (hn : 0 < n) (h : x < 1) :
x ^ n < 1
source
theorem Right.nsmul_neg {M : Type u_3} [AddMonoid M] [Preorder M] [AddRightMono M] {n : ℕ} {x : M} (hn : 0 < n) (h : x < 0) :
n • x < 0
source
theorem pow_le_pow_mul_of_sq_le_mul {M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] [MulLeftMono M] {a b : M} (hab : a ^ 2 ≤ b * a) {n : ℕ} :
n ≠ 0 → a ^ n ≤ b ^ (n - 1) * a

This lemma is useful in non-cancellative monoids, like sets under pointwise operations.

source
theorem nsmul_le_nsmul_add_of_sq_le_add {M : Type u_3} [AddMonoid M] [Preorder M] [AddRightMono M] [AddLeftMono M] {a b : M} (hab : 2 • a ≤ b + a) {n : ℕ} :
n ≠ 0 → n • a ≤ (n - 1) • b + a

This lemma is useful in non-cancellative monoids, like sets under pointwise operations.

source
theorem StrictMono.pow_const {β : Type u_1} {M : Type u_3} [Monoid M] [Preorder M] [Preorder β] [MulLeftStrictMono M] [MulRightStrictMono M] {f : β → M} (hf : StrictMono f) {n : ℕ} :
n ≠ 0 → StrictMono fun (x : β) => f x ^ n
source
theorem StrictMono.const_nsmul {β : Type u_1} {M : Type u_3} [AddMonoid M] [Preorder M] [Preorder β] [AddLeftStrictMono M] [AddRightStrictMono M] {f : β → M} (hf : StrictMono f) {n : ℕ} :
n ≠ 0 → StrictMono fun (x : β) => n • f x
source
theorem pow_left_strictMono {M : Type u_3} [Monoid M] [Preorder M] [MulLeftStrictMono M] [MulRightStrictMono M] {n : ℕ} (hn : n ≠ 0) :
StrictMono fun (x : M) => x ^ n

See also pow_left_strictMonoOn₀.

source
theorem nsmul_right_strictMono {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddRightStrictMono M] {n : ℕ} (hn : n ≠ 0) :
StrictMono fun (x : M) => n • x
source
theorem pow_lt_pow_left' {M : Type u_3} [Monoid M] [Preorder M] [MulLeftStrictMono M] [MulRightStrictMono M] {n : ℕ} (hn : n ≠ 0) {a b : M} (hab : a < b) :
a ^ n < b ^ n
source
theorem nsmul_lt_nsmul_right {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddRightStrictMono M] {n : ℕ} (hn : n ≠ 0) {a b : M} (hab : a < b) :
n • a < n • b
source
theorem pow_le_pow_left' {M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] [MulRightMono M] {a b : M} (hab : a ≤ b) (i : ℕ) :
a ^ i ≤ b ^ i
source
theorem nsmul_le_nsmul_right {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftMono M] [AddRightMono M] {a b : M} (hab : a ≤ b) (i : ℕ) :
i • a ≤ i • b
source
theorem Monotone.pow_const {β : Type u_1} {M : Type u_3} [Monoid M] [Preorder M] [Preorder β] [MulLeftMono M] [MulRightMono M] {f : β → M} (hf : Monotone f) (n : ℕ) :
Monotone fun (a : β) => f a ^ n
source
theorem Monotone.const_nsmul {β : Type u_1} {M : Type u_3} [AddMonoid M] [Preorder M] [Preorder β] [AddLeftMono M] [AddRightMono M] {f : β → M} (hf : Monotone f) (n : ℕ) :
Monotone fun (a : β) => n • f a
source
theorem pow_left_mono {M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] [MulRightMono M] (n : ℕ) :
Monotone fun (a : M) => a ^ n
source
theorem nsmul_right_mono {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftMono M] [AddRightMono M] (n : ℕ) :
Monotone fun (a : M) => n • a
source
theorem pow_le_pow {M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] [MulRightMono M] {a b : M} (hab : a ≤ b) (ht : 1 ≤ b) {m n : ℕ} (hmn : m ≤ n) :
a ^ m ≤ b ^ n
source
theorem nsmul_le_nsmul {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftMono M] [AddRightMono M] {a b : M} (hab : a ≤ b) (ht : 0 ≤ b) {m n : ℕ} (hmn : m ≤ n) :
m • a ≤ n • b
source
theorem le_pow_sup {M : Type u_3} [Monoid M] [SemilatticeSup M] [MulLeftMono M] [MulRightMono M] {a b : M} {n : ℕ} :
a ^ n ⊔ b ^ n ≤ (a ⊔ b) ^ n
source
theorem pow_inf_le {M : Type u_3} [Monoid M] [SemilatticeInf M] [MulLeftMono M] [MulRightMono M] {a b : M} {n : ℕ} :
(a ⊓ b) ^ n ≤ a ^ n ⊓ b ^ n
source
theorem one_le_pow_iff {M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftMono M] {x : M} {n : ℕ} (hn : n ≠ 0) :
1 ≤ x ^ n ↔ 1 ≤ x
source
theorem nsmul_nonneg_iff {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftMono M] {x : M} {n : ℕ} (hn : n ≠ 0) :
0 ≤ n • x ↔ 0 ≤ x
source
theorem pow_le_one_iff {M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftMono M] {x : M} {n : ℕ} (hn : n ≠ 0) :
x ^ n ≤ 1 ↔ x ≤ 1
source
theorem nsmul_nonpos_iff {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftMono M] {x : M} {n : ℕ} (hn : n ≠ 0) :
n • x ≤ 0 ↔ x ≤ 0
source
theorem one_lt_pow_iff {M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftMono M] {x : M} {n : ℕ} (hn : n ≠ 0) :
1 < x ^ n ↔ 1 < x
source
theorem nsmul_pos_iff {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftMono M] {x : M} {n : ℕ} (hn : n ≠ 0) :
0 < n • x ↔ 0 < x
source
theorem pow_lt_one_iff {M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftMono M] {x : M} {n : ℕ} (hn : n ≠ 0) :
x ^ n < 1 ↔ x < 1
source
theorem nsmul_neg_iff {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftMono M] {x : M} {n : ℕ} (hn : n ≠ 0) :
n • x < 0 ↔ x < 0
source
theorem pow_le_pow_iff_right' {M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftStrictMono M] {a : M} {m n : ℕ} (ha : 1 < a) :
a ^ m ≤ a ^ n ↔ m ≤ n
source
theorem nsmul_le_nsmul_iff_left {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] {a : M} {m n : ℕ} (ha : 0 < a) :
m • a ≤ n • a ↔ m ≤ n
source
theorem pow_lt_pow_iff_right' {M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftStrictMono M] {a : M} {m n : ℕ} (ha : 1 < a) :
a ^ m < a ^ n ↔ m < n
source
theorem nsmul_lt_nsmul_iff_left {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] {a : M} {m n : ℕ} (ha : 0 < a) :
m • a < n • a ↔ m < n
source
theorem lt_of_pow_lt_pow_left' {M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftMono M] [MulRightMono M] {a b : M} (n : ℕ) :
a ^ n < b ^ n → a < b
source
theorem lt_of_nsmul_lt_nsmul_right {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftMono M] [AddRightMono M] {a b : M} (n : ℕ) :
n • a < n • b → a < b
source
theorem min_lt_of_mul_lt_sq {M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftMono M] [MulRightMono M] {a b c : M} (h : a * b < c ^ 2) :
min a b < c
source
theorem min_lt_of_add_lt_two_nsmul {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftMono M] [AddRightMono M] {a b c : M} (h : a + b < 2 • c) :
min a b < c
source
theorem lt_max_of_sq_lt_mul {M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftMono M] [MulRightMono M] {a b c : M} (h : a ^ 2 < b * c) :
a < max b c
source
theorem lt_max_of_two_nsmul_lt_add {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftMono M] [AddRightMono M] {a b c : M} (h : 2 • a < b + c) :
a < max b c
source
theorem pow_le_pow_iff_left {M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftStrictMono M] [MulRightStrictMono M] {a b : M} {n : ℕ} (hn : n ≠ 0) :
a ^ n ≤ b ^ n ↔ a ≤ b
source
theorem nsmul_le_nsmul_iff_right {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] [AddRightStrictMono M] {a b : M} {n : ℕ} (hn : n ≠ 0) :
n • a ≤ n • b ↔ a ≤ b
source
theorem le_of_pow_le_pow_left' {M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftStrictMono M] [MulRightStrictMono M] {a b : M} {n : ℕ} (hn : n ≠ 0) :
a ^ n ≤ b ^ n → a ≤ b

Alias of the forward direction of pow_le_pow_iff_left.

source
theorem le_of_nsmul_le_nsmul_right {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] [AddRightStrictMono M] {a b : M} {n : ℕ} (hn : n ≠ 0) :
n • a ≤ n • b → a ≤ b

Alias of the forward direction of nsmul_le_nsmul_iff_right.

source
theorem min_le_of_mul_le_sq {M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftStrictMono M] [MulRightStrictMono M] {a b c : M} (h : a * b ≤ c ^ 2) :
min a b ≤ c
source
theorem min_le_of_add_le_two_nsmul {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] [AddRightStrictMono M] {a b c : M} (h : a + b ≤ 2 • c) :
min a b ≤ c
source
theorem le_max_of_sq_le_mul {M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftStrictMono M] [MulRightStrictMono M] {a b c : M} (h : a ^ 2 ≤ b * c) :
a ≤ max b c
source
theorem le_max_of_two_nsmul_le_add {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] [AddRightStrictMono M] {a b c : M} (h : 2 • a ≤ b + c) :
a ≤ max b c
source
theorem Left.pow_lt_one_iff' {M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftStrictMono M] {n : ℕ} {x : M} (hn : 0 < n) :
x ^ n < 1 ↔ x < 1
source
theorem Left.nsmul_neg_iff {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] {n : ℕ} {x : M} (hn : 0 < n) :
n • x < 0 ↔ x < 0
source
theorem Left.pow_lt_one_iff {M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftStrictMono M] {n : ℕ} {x : M} (hn : 0 < n) :
x ^ n < 1 ↔ x < 1
source
theorem Right.pow_lt_one_iff {M : Type u_3} [Monoid M] [LinearOrder M] [MulRightStrictMono M] {n : ℕ} {x : M} (hn : 0 < n) :
x ^ n < 1 ↔ x < 1
source
theorem Right.nsmul_neg_iff {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddRightStrictMono M] {n : ℕ} {x : M} (hn : 0 < n) :
n • x < 0 ↔ x < 0
source
instance instHasUniqueRootsOfMulLeftStrictMonoOfMulRightStrictMono {M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftStrictMono M] [MulRightStrictMono M] :
HasUniqueRoots M
source
instance insthasUniqueDivOfAddLeftStrictMonoOfAddRightStrictMono {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] [AddRightStrictMono M] :
HasUniqueDiv M
source
theorem one_le_zpow {G : Type u_2} [DivInvMonoid G] [Preorder G] [MulLeftMono G] {x : G} (H : 1 ≤ x) {n : ℤ} (hn : 0 ≤ n) :
1 ≤ x ^ n
source
theorem zsmul_nonneg {G : Type u_2} [SubNegMonoid G] [Preorder G] [AddLeftMono G] {x : G} (H : 0 ≤ x) {n : ℤ} (hn : 0 ≤ n) :
0 ≤ n • x
source
theorem one_lt_zpow {G : Type u_2} [DivInvMonoid G] [Preorder G] [MulLeftMono G] {x : G} (hx : 1 < x) {n : ℤ} (hn : 0 < n) :
1 < x ^ n
source
theorem zsmul_pos {G : Type u_2} [SubNegMonoid G] [Preorder G] [AddLeftMono G] {x : G} (hx : 0 < x) {n : ℤ} (hn : 0 < n) :
0 < n • x