mathlib documentation

algebra.group_power.order

Lemmas about the interaction of power operations with order #

Note that some lemmas are in algebra/group_power/lemmas.lean as they import files which depend on this file.

source
theorem nsmul_le_nsmul_of_le_right {M : Type u_3} [add_monoid M] [preorder M] [covariant_class M M has_add.add has_le.le] [covariant_class M M (function.swap has_add.add) has_le.le] {a b : M} (hab : a ≤ b) (i : ℕ) :
i • a ≤ i • b
source
theorem pow_le_pow_of_le_left' {M : Type u_3} [monoid M] [preorder M] [covariant_class M M has_mul.mul has_le.le] [covariant_class M M (function.swap has_mul.mul) has_le.le] {a b : M} (hab : a ≤ b) (i : ℕ) :
a ^ i ≤ b ^ i
source
theorem one_le_pow_of_one_le' {M : Type u_3} [monoid M] [preorder M] [covariant_class M M has_mul.mul has_le.le] {a : M} (H : 1 ≤ a) (n : ℕ) :
1 ≤ a ^ n
source
theorem nsmul_nonneg {M : Type u_3} [add_monoid M] [preorder M] [covariant_class M M has_add.add has_le.le] {a : M} (H : 0 ≤ a) (n : ℕ) :
0 ≤ n • a
source
theorem pow_le_one' {M : Type u_3} [monoid M] [preorder M] [covariant_class M M has_mul.mul has_le.le] {a : M} (H : a ≤ 1) (n : ℕ) :
a ^ n ≤ 1
source
theorem nsmul_nonpos {M : Type u_3} [add_monoid M] [preorder M] [covariant_class M M has_add.add has_le.le] {a : M} (H : a ≤ 0) (n : ℕ) :
n • a ≤ 0
source
theorem pow_le_pow' {M : Type u_3} [monoid M] [preorder M] [covariant_class M M has_mul.mul has_le.le] {a : M} {n m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) :
a ^ n ≤ a ^ m
source
theorem nsmul_le_nsmul {M : Type u_3} [add_monoid M] [preorder M] [covariant_class M M has_add.add has_le.le] {a : M} {n m : ℕ} (ha : 0 ≤ a) (h : n ≤ m) :
n • a ≤ m • a
source
theorem nsmul_le_nsmul_of_nonpos {M : Type u_3} [add_monoid M] [preorder M] [covariant_class M M has_add.add has_le.le] {a : M} {n m : ℕ} (ha : a ≤ 0) (h : n ≤ m) :
m • a ≤ n • a
source
theorem pow_le_pow_of_le_one' {M : Type u_3} [monoid M] [preorder M] [covariant_class M M has_mul.mul has_le.le] {a : M} {n m : ℕ} (ha : a ≤ 1) (h : n ≤ m) :
a ^ m ≤ a ^ n
source
theorem one_lt_pow' {M : Type u_3} [monoid M] [preorder M] [covariant_class M M has_mul.mul has_le.le] {a : M} (ha : 1 < a) {k : ℕ} (hk : k ≠ 0) :
1 < a ^ k
source
theorem nsmul_pos {M : Type u_3} [add_monoid M] [preorder M] [covariant_class M M has_add.add has_le.le] {a : M} (ha : 0 < a) {k : ℕ} (hk : k ≠ 0) :
0 < k • a
source
theorem pow_lt_one' {M : Type u_3} [monoid M] [preorder M] [covariant_class M M has_mul.mul has_le.le] {a : M} (ha : a < 1) {k : ℕ} (hk : k ≠ 0) :
a ^ k < 1
source
theorem nsmul_neg {M : Type u_3} [add_monoid M] [preorder M] [covariant_class M M has_add.add has_le.le] {a : M} (ha : a < 0) {k : ℕ} (hk : k ≠ 0) :
k • a < 0
source
theorem pow_lt_pow' {M : Type u_3} [monoid M] [preorder M] [covariant_class M M has_mul.mul has_le.le] [covariant_class M M has_mul.mul has_lt.lt] {a : M} {n m : ℕ} (ha : 1 < a) (h : n < m) :
a ^ n < a ^ m
source
theorem nsmul_lt_nsmul {M : Type u_3} [add_monoid M] [preorder M] [covariant_class M M has_add.add has_le.le] [covariant_class M M has_add.add has_lt.lt] {a : M} {n m : ℕ} (ha : 0 < a) (h : n < m) :
n • a < m • a
source
theorem nsmul_nonneg_iff {M : Type u_3} [add_monoid M] [linear_order M] [covariant_class M M has_add.add has_le.le] {x : M} {n : ℕ} (hn : n ≠ 0) :
0 ≤ n • x ↔ 0 ≤ x
source
theorem one_le_pow_iff {M : Type u_3} [monoid M] [linear_order M] [covariant_class M M has_mul.mul has_le.le] {x : M} {n : ℕ} (hn : n ≠ 0) :
1 ≤ x ^ n ↔ 1 ≤ x
source
theorem nsmul_nonpos_iff {M : Type u_3} [add_monoid M] [linear_order M] [covariant_class M M has_add.add has_le.le] {x : M} {n : ℕ} (hn : n ≠ 0) :
n • x ≤ 0 ↔ x ≤ 0
source
theorem pow_le_one_iff {M : Type u_3} [monoid M] [linear_order M] [covariant_class M M has_mul.mul has_le.le] {x : M} {n : ℕ} (hn : n ≠ 0) :
x ^ n ≤ 1 ↔ x ≤ 1
source
theorem one_lt_pow_iff {M : Type u_3} [monoid M] [linear_order M] [covariant_class M M has_mul.mul has_le.le] {x : M} {n : ℕ} (hn : n ≠ 0) :
1 < x ^ n ↔ 1 < x
source
theorem nsmul_pos_iff {M : Type u_3} [add_monoid M] [linear_order M] [covariant_class M M has_add.add has_le.le] {x : M} {n : ℕ} (hn : n ≠ 0) :
0 < n • x ↔ 0 < x
source
theorem pow_lt_one_iff {M : Type u_3} [monoid M] [linear_order M] [covariant_class M M has_mul.mul has_le.le] {x : M} {n : ℕ} (hn : n ≠ 0) :
x ^ n < 1 ↔ x < 1
source
theorem nsmul_neg_iff {M : Type u_3} [add_monoid M] [linear_order M] [covariant_class M M has_add.add has_le.le] {x : M} {n : ℕ} (hn : n ≠ 0) :
n • x < 0 ↔ x < 0
source
theorem pow_eq_one_iff {M : Type u_3} [monoid M] [linear_order M] [covariant_class M M has_mul.mul has_le.le] {x : M} {n : ℕ} (hn : n ≠ 0) :
x ^ n = 1 ↔ x = 1
source
theorem nsmul_eq_zero_iff {M : Type u_3} [add_monoid M] [linear_order M] [covariant_class M M has_add.add has_le.le] {x : M} {n : ℕ} (hn : n ≠ 0) :
n • x = 0 ↔ x = 0
source
theorem one_le_zpow {G : Type u_2} [div_inv_monoid G] [preorder G] [covariant_class G G has_mul.mul has_le.le] {x : G} (H : 1 ≤ x) {n : ℤ} (hn : 0 ≤ n) :
1 ≤ x ^ n
source
theorem zsmul_nonneg {G : Type u_2} [sub_neg_monoid G] [preorder G] [covariant_class G G has_add.add has_le.le] {x : G} (H : 0 ≤ x) {n : ℤ} (hn : 0 ≤ n) :
0 ≤ n • x
source
theorem canonically_ordered_comm_semiring.pow_pos {R : Type u_4} [canonically_ordered_comm_semiring R] {a : R} (H : 0 < a) (n : ℕ) :
0 < a ^ n
source
theorem pow_add_pow_le {R : Type u_4} [ordered_semiring R] {x y : R} {n : ℕ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hn : n ≠ 0) :
x ^ n + y ^ n ≤ (x + y) ^ n
source
theorem pow_lt_pow_of_lt_left {R : Type u_4} [ordered_semiring R] {x y : R} {n : ℕ} (Hxy : x < y) (Hxpos : 0 ≤ x) (Hnpos : 0 < n) :
x ^ n < y ^ n
source
theorem pow_lt_one {R : Type u_4} [ordered_semiring R] {a : R} (h₀ : 0 ≤ a) (h₁ : a < 1) {n : ℕ} (hn : n ≠ 0) :
a ^ n < 1
source
theorem strict_mono_on_pow {R : Type u_4} [ordered_semiring R] {n : ℕ} (hn : 0 < n) :
strict_mono_on (λ (x : R), x ^ n) (set.Ici 0)
source
theorem one_le_pow_of_one_le {R : Type u_4} [ordered_semiring R] {a : R} (H : 1 ≤ a) (n : ℕ) :
1 ≤ a ^ n
source
theorem pow_mono {R : Type u_4} [ordered_semiring R] {a : R} (h : 1 ≤ a) :
monotone (λ (n : ℕ), a ^ n)
source
theorem pow_le_pow {R : Type u_4} [ordered_semiring R] {a : R} {n m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) :
a ^ n ≤ a ^ m
source
theorem le_self_pow {R : Type u_4} [ordered_semiring R] {a : R} {m : ℕ} (ha : 1 ≤ a) (h : 1 ≤ m) :
a ≤ a ^ m
source
theorem strict_mono_pow {R : Type u_4} [ordered_semiring R] {a : R} (h : 1 < a) :
strict_mono (λ (n : ℕ), a ^ n)
source
theorem pow_lt_pow {R : Type u_4} [ordered_semiring R] {a : R} {n m : ℕ} (h : 1 < a) (h2 : n < m) :
a ^ n < a ^ m
source
theorem pow_lt_pow_iff {R : Type u_4} [ordered_semiring R] {a : R} {n m : ℕ} (h : 1 < a) :
a ^ n < a ^ m ↔ n < m
source
theorem pow_le_pow_iff {R : Type u_4} [ordered_semiring R] {a : R} {n m : ℕ} (h : 1 < a) :
a ^ n ≤ a ^ m ↔ n ≤ m
source
theorem strict_anti_pow {R : Type u_4} [ordered_semiring R] {a : R} (h₀ : 0 < a) (h₁ : a < 1) :
strict_anti (λ (n : ℕ), a ^ n)
source
theorem pow_lt_pow_iff_of_lt_one {R : Type u_4} [ordered_semiring R] {a : R} {n m : ℕ} (h₀ : 0 < a) (h₁ : a < 1) :
a ^ m < a ^ n ↔ n < m
source
theorem pow_lt_pow_of_lt_one {R : Type u_4} [ordered_semiring R] {a : R} (h : 0 < a) (ha : a < 1) {i j : ℕ} (hij : i < j) :
a ^ j < a ^ i
source
theorem pow_le_pow_of_le_left {R : Type u_4} [ordered_semiring R] {a b : R} (ha : 0 ≤ a) (hab : a ≤ b) (i : ℕ) :
a ^ i ≤ b ^ i
source
theorem one_lt_pow {R : Type u_4} [ordered_semiring R] {a : R} (ha : 1 < a) {n : ℕ} (hn : n ≠ 0) :
1 < a ^ n
source
theorem pow_le_one {R : Type u_4} [ordered_semiring R] {a : R} (n : ℕ) (h₀ : 0 ≤ a) (h₁ : a ≤ 1) :
a ^ n ≤ 1
source
theorem sq_pos_of_pos {R : Type u_4} [ordered_semiring R] {a : R} (ha : 0 < a) :
0 < a ^ 2
source
theorem sq_pos_of_neg {R : Type u_4} [ordered_ring R] {a : R} (ha : a < 0) :
0 < a ^ 2
source
theorem pow_bit0_pos_of_neg {R : Type u_4} [ordered_ring R] {a : R} (ha : a < 0) (n : ℕ) :
0 < a ^ bit0 n
source
theorem pow_bit1_neg {R : Type u_4} [ordered_ring R] {a : R} (ha : a < 0) (n : ℕ) :
a ^ bit1 n < 0
source
theorem pow_le_one_iff_of_nonneg {R : Type u_4} [linear_ordered_semiring R] {a : R} (ha : 0 ≤ a) {n : ℕ} (hn : n ≠ 0) :
a ^ n ≤ 1 ↔ a ≤ 1
source
theorem one_le_pow_iff_of_nonneg {R : Type u_4} [linear_ordered_semiring R] {a : R} (ha : 0 ≤ a) {n : ℕ} (hn : n ≠ 0) :
1 ≤ a ^ n ↔ 1 ≤ a
source
theorem one_lt_pow_iff_of_nonneg {R : Type u_4} [linear_ordered_semiring R] {a : R} (ha : 0 ≤ a) {n : ℕ} (hn : n ≠ 0) :
1 < a ^ n ↔ 1 < a
source
theorem pow_lt_one_iff_of_nonneg {R : Type u_4} [linear_ordered_semiring R] {a : R} (ha : 0 ≤ a) {n : ℕ} (hn : n ≠ 0) :
a ^ n < 1 ↔ a < 1
source
theorem sq_le_one_iff {R : Type u_4} [linear_ordered_semiring R] {a : R} (ha : 0 ≤ a) :
a ^ 2 ≤ 1 ↔ a ≤ 1
source
theorem sq_lt_one_iff {R : Type u_4} [linear_ordered_semiring R] {a : R} (ha : 0 ≤ a) :
a ^ 2 < 1 ↔ a < 1
source
theorem one_le_sq_iff {R : Type u_4} [linear_ordered_semiring R] {a : R} (ha : 0 ≤ a) :
1 ≤ a ^ 2 ↔ 1 ≤ a
source
theorem one_lt_sq_iff {R : Type u_4} [linear_ordered_semiring R] {a : R} (ha : 0 ≤ a) :
1 < a ^ 2 ↔ 1 < a
source
@[simp]
theorem pow_left_inj {R : Type u_4} [linear_ordered_semiring R] {x y : R} {n : ℕ} (Hxpos : 0 ≤ x) (Hypos : 0 ≤ y) (Hnpos : 0 < n) :
x ^ n = y ^ n ↔ x = y
source
theorem lt_of_pow_lt_pow {R : Type u_4} [linear_ordered_semiring R] {a b : R} (n : ℕ) (hb : 0 ≤ b) (h : a ^ n < b ^ n) :
a < b
source
theorem le_of_pow_le_pow {R : Type u_4} [linear_ordered_semiring R] {a b : R} (n : ℕ) (hb : 0 ≤ b) (hn : 0 < n) (h : a ^ n ≤ b ^ n) :
a ≤ b
source
@[simp]
theorem sq_eq_sq {R : Type u_4} [linear_ordered_semiring R] {a b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) :
a ^ 2 = b ^ 2 ↔ a = b
source
theorem pow_abs {R : Type u_4} [linear_ordered_ring R] (a : R) (n : ℕ) :
|a| ^ n = |a ^ n|
source
theorem abs_neg_one_pow {R : Type u_4} [linear_ordered_ring R] (n : ℕ) :
|(-1) ^ n| = 1
source
theorem pow_bit0_nonneg {R : Type u_4} [linear_ordered_ring R] (a : R) (n : ℕ) :
0 ≤ a ^ bit0 n
source
theorem sq_nonneg {R : Type u_4} [linear_ordered_ring R] (a : R) :
0 ≤ a ^ 2
source
theorem pow_two_nonneg {R : Type u_4} [linear_ordered_ring R] (a : R) :
0 ≤ a ^ 2

Alias of sq_nonneg.

source
theorem pow_bit0_pos {R : Type u_4} [linear_ordered_ring R] {a : R} (h : a ≠ 0) (n : ℕ) :
0 < a ^ bit0 n
source
theorem sq_pos_of_ne_zero {R : Type u_4} [linear_ordered_ring R] (a : R) (h : a ≠ 0) :
0 < a ^ 2
source
theorem pow_two_pos_of_ne_zero {R : Type u_4} [linear_ordered_ring R] (a : R) (h : a ≠ 0) :
0 < a ^ 2

Alias of sq_pos_of_ne_zero.

source
theorem pow_bit0_pos_iff {R : Type u_4} [linear_ordered_ring R] (a : R) {n : ℕ} (hn : n ≠ 0) :
0 < a ^ bit0 n ↔ a ≠ 0
source
theorem sq_pos_iff {R : Type u_4} [linear_ordered_ring R] (a : R) :
0 < a ^ 2 ↔ a ≠ 0
source
theorem sq_abs {R : Type u_4} [linear_ordered_ring R] (x : R) :
|x| ^ 2 = x ^ 2
source
theorem abs_sq {R : Type u_4} [linear_ordered_ring R] (x : R) :
|x ^ 2| = x ^ 2
source
theorem sq_lt_sq {R : Type u_4} [linear_ordered_ring R] {x y : R} (h : |x| < |y|) :
x ^ 2 < y ^ 2
source
theorem sq_lt_sq' {R : Type u_4} [linear_ordered_ring R] {x y : R} (h1 : -y < x) (h2 : x < y) :
x ^ 2 < y ^ 2
source
theorem sq_le_sq {R : Type u_4} [linear_ordered_ring R] {x y : R} (h : |x| ≤ |y|) :
x ^ 2 ≤ y ^ 2
source
theorem sq_le_sq' {R : Type u_4} [linear_ordered_ring R] {x y : R} (h1 : -y ≤ x) (h2 : x ≤ y) :
x ^ 2 ≤ y ^ 2
source
theorem abs_lt_abs_of_sq_lt_sq {R : Type u_4} [linear_ordered_ring R] {x y : R} (h : x ^ 2 < y ^ 2) :
|x| < |y|
source
theorem abs_lt_of_sq_lt_sq {R : Type u_4} [linear_ordered_ring R] {x y : R} (h : x ^ 2 < y ^ 2) (hy : 0 ≤ y) :
|x| < y
source
theorem abs_lt_of_sq_lt_sq' {R : Type u_4} [linear_ordered_ring R] {x y : R} (h : x ^ 2 < y ^ 2) (hy : 0 ≤ y) :
-y < x ∧ x < y
source
theorem abs_le_abs_of_sq_le_sq {R : Type u_4} [linear_ordered_ring R] {x y : R} (h : x ^ 2 ≤ y ^ 2) :
|x| ≤ |y|
source
theorem abs_le_of_sq_le_sq {R : Type u_4} [linear_ordered_ring R] {x y : R} (h : x ^ 2 ≤ y ^ 2) (hy : 0 ≤ y) :
|x| ≤ y
source
theorem abs_le_of_sq_le_sq' {R : Type u_4} [linear_ordered_ring R] {x y : R} (h : x ^ 2 ≤ y ^ 2) (hy : 0 ≤ y) :
-y ≤ x ∧ x ≤ y
source
theorem sq_eq_sq_iff_abs_eq_abs {R : Type u_4} [linear_ordered_ring R] (x y : R) :
x ^ 2 = y ^ 2 ↔ |x| = |y|
source
@[simp]
theorem sq_eq_one_iff {R : Type u_4} [linear_ordered_ring R] (x : R) :
x ^ 2 = 1 ↔ x = 1 ∨ x = -1
source
theorem sq_ne_one_iff {R : Type u_4} [linear_ordered_ring R] (x : R) :
x ^ 2 ≠ 1 ↔ x ≠ 1 ∧ x ≠ -1
source
@[simp]
theorem sq_le_one_iff_abs_le_one {R : Type u_4} [linear_ordered_ring R] (x : R) :
x ^ 2 ≤ 1 ↔ |x| ≤ 1
source
@[simp]
theorem sq_lt_one_iff_abs_lt_one {R : Type u_4} [linear_ordered_ring R] (x : R) :
x ^ 2 < 1 ↔ |x| < 1
source
@[simp]
theorem one_le_sq_iff_one_le_abs {R : Type u_4} [linear_ordered_ring R] (x : R) :
1 ≤ x ^ 2 ↔ 1 ≤ |x|
source
@[simp]
theorem one_lt_sq_iff_one_lt_abs {R : Type u_4} [linear_ordered_ring R] (x : R) :
1 < x ^ 2 ↔ 1 < |x|
source
theorem two_mul_le_add_sq {R : Type u_4} [linear_ordered_comm_ring R] (a b : R) :
(2 * a) * b ≤ a ^ 2 + b ^ 2

Arithmetic mean-geometric mean (AM-GM) inequality for linearly ordered commutative rings.

source
theorem two_mul_le_add_pow_two {R : Type u_4} [linear_ordered_comm_ring R] (a b : R) :
(2 * a) * b ≤ a ^ 2 + b ^ 2

Alias of two_mul_le_add_sq.