Lemmas about the interaction of power operations with order #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Note that some lemmas are in algebra/group_power/lemmas.lean as they import files which
depend on this file.
theorem
nsmul_le_nsmul_of_le_right
{M : Type u_4}
[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 : ℕ) :
theorem
pow_le_pow_of_le_left'
{M : Type u_4}
[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 : ℕ) :
theorem
one_le_pow_of_one_le'
{M : Type u_4}
[monoid M]
[preorder M]
[covariant_class M M has_mul.mul has_le.le]
{a : M}
(H : 1 ≤ a)
(n : ℕ) :
theorem
nsmul_nonneg
{M : Type u_4}
[add_monoid M]
[preorder M]
[covariant_class M M has_add.add has_le.le]
{a : M}
(H : 0 ≤ a)
(n : ℕ) :
theorem
pow_le_one'
{M : Type u_4}
[monoid M]
[preorder M]
[covariant_class M M has_mul.mul has_le.le]
{a : M}
(H : a ≤ 1)
(n : ℕ) :
theorem
nsmul_nonpos
{M : Type u_4}
[add_monoid M]
[preorder M]
[covariant_class M M has_add.add has_le.le]
{a : M}
(H : a ≤ 0)
(n : ℕ) :
theorem
pow_le_pow'
{M : Type u_4}
[monoid M]
[preorder M]
[covariant_class M M has_mul.mul has_le.le]
{a : M}
{n m : ℕ}
(ha : 1 ≤ a)
(h : n ≤ m) :
theorem
nsmul_le_nsmul
{M : Type u_4}
[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) :
theorem
nsmul_le_nsmul_of_nonpos
{M : Type u_4}
[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) :
theorem
pow_le_pow_of_le_one'
{M : Type u_4}
[monoid M]
[preorder M]
[covariant_class M M has_mul.mul has_le.le]
{a : M}
{n m : ℕ}
(ha : a ≤ 1)
(h : n ≤ m) :
theorem
one_lt_pow'
{M : Type u_4}
[monoid M]
[preorder M]
[covariant_class M M has_mul.mul has_le.le]
{a : M}
(ha : 1 < a)
{k : ℕ}
(hk : k ≠ 0) :
theorem
nsmul_pos
{M : Type u_4}
[add_monoid M]
[preorder M]
[covariant_class M M has_add.add has_le.le]
{a : M}
(ha : 0 < a)
{k : ℕ}
(hk : k ≠ 0) :
theorem
pow_lt_one'
{M : Type u_4}
[monoid M]
[preorder M]
[covariant_class M M has_mul.mul has_le.le]
{a : M}
(ha : a < 1)
{k : ℕ}
(hk : k ≠ 0) :
theorem
nsmul_neg
{M : Type u_4}
[add_monoid M]
[preorder M]
[covariant_class M M has_add.add has_le.le]
{a : M}
(ha : a < 0)
{k : ℕ}
(hk : k ≠ 0) :
theorem
pow_lt_pow'
{M : Type u_4}
[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) :
theorem
nsmul_lt_nsmul
{M : Type u_4}
[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) :
theorem
nsmul_strict_mono_right
{M : Type u_4}
[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}
(ha : 0 < a) :
strict_mono (λ (ᾰ : ℕ), ᾰ • a)
theorem
pow_strict_mono_left
{M : Type u_4}
[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}
(ha : 1 < a) :
theorem
left.one_le_pow_of_le
{M : Type u_4}
[monoid M]
[preorder M]
[covariant_class M M has_mul.mul has_le.le]
{x : M}
(hx : 1 ≤ x)
{n : ℕ} :
theorem
left.pow_nonneg
{M : Type u_4}
[add_monoid M]
[preorder M]
[covariant_class M M has_add.add has_le.le]
{x : M}
(hx : 0 ≤ x)
{n : ℕ} :
theorem
left.pow_le_one_of_le
{M : Type u_4}
[monoid M]
[preorder M]
[covariant_class M M has_mul.mul has_le.le]
{x : M}
(hx : x ≤ 1)
{n : ℕ} :
theorem
left.pow_nonpos
{M : Type u_4}
[add_monoid M]
[preorder M]
[covariant_class M M has_add.add has_le.le]
{x : M}
(hx : x ≤ 0)
{n : ℕ} :
theorem
right.one_le_pow_of_le
{M : Type u_4}
[monoid M]
[preorder M]
[covariant_class M M (function.swap has_mul.mul) has_le.le]
{x : M}
(hx : 1 ≤ x)
{n : ℕ} :
theorem
right.pow_nonneg
{M : Type u_4}
[add_monoid M]
[preorder M]
[covariant_class M M (function.swap has_add.add) has_le.le]
{x : M}
(hx : 0 ≤ x)
{n : ℕ} :
theorem
right.pow_nonpos
{M : Type u_4}
[add_monoid M]
[preorder M]
[covariant_class M M (function.swap has_add.add) has_le.le]
{x : M}
(hx : x ≤ 0)
{n : ℕ} :
theorem
right.pow_le_one_of_le
{M : Type u_4}
[monoid M]
[preorder M]
[covariant_class M M (function.swap has_mul.mul) has_le.le]
{x : M}
(hx : x ≤ 1)
{n : ℕ} :
theorem
strict_mono.pow_right'
{β : Type u_1}
{M : Type u_4}
[monoid M]
[preorder M]
[preorder β]
[covariant_class M M has_mul.mul has_lt.lt]
[covariant_class M M (function.swap has_mul.mul) has_lt.lt]
{f : β → M}
(hf : strict_mono f)
{n : ℕ} :
n ≠ 0 → strict_mono (λ (a : β), f a ^ n)
theorem
strict_mono.nsmul_left
{β : Type u_1}
{M : Type u_4}
[add_monoid M]
[preorder M]
[preorder β]
[covariant_class M M has_add.add has_lt.lt]
[covariant_class M M (function.swap has_add.add) has_lt.lt]
{f : β → M}
(hf : strict_mono f)
{n : ℕ} :
n ≠ 0 → strict_mono (λ (a : β), n • f a)
@[nolint]
theorem
pow_strict_mono_right'
{M : Type u_4}
[monoid M]
[preorder M]
[covariant_class M M has_mul.mul has_lt.lt]
[covariant_class M M (function.swap has_mul.mul) has_lt.lt]
{n : ℕ}
(hn : n ≠ 0) :
strict_mono (λ (a : M), a ^ n)
See also pow_strict_mono_right
@[nolint]
theorem
nsmul_strict_mono_left
{M : Type u_4}
[add_monoid M]
[preorder M]
[covariant_class M M has_add.add has_lt.lt]
[covariant_class M M (function.swap has_add.add) has_lt.lt]
{n : ℕ}
(hn : n ≠ 0) :
strict_mono (λ (a : M), n • a)
theorem
monotone.pow_right
{β : Type u_1}
{M : Type u_4}
[monoid M]
[preorder M]
[preorder β]
[covariant_class M M has_mul.mul has_le.le]
[covariant_class M M (function.swap has_mul.mul) has_le.le]
{f : β → M}
(hf : monotone f)
(n : ℕ) :
theorem
monotone.nsmul_left
{β : Type u_1}
{M : Type u_4}
[add_monoid M]
[preorder M]
[preorder β]
[covariant_class M M has_add.add has_le.le]
[covariant_class M M (function.swap has_add.add) has_le.le]
{f : β → M}
(hf : monotone f)
(n : ℕ) :
theorem
pow_mono_right
{M : Type u_4}
[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]
(n : ℕ) :
theorem
nsmul_mono_left
{M : Type u_4}
[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]
(n : ℕ) :
theorem
left.pow_neg
{M : Type u_4}
[add_monoid M]
[preorder M]
[covariant_class M M has_add.add has_lt.lt]
{n : ℕ}
{x : M}
(hn : 0 < n)
(h : x < 0) :
theorem
left.pow_lt_one_of_lt
{M : Type u_4}
[monoid M]
[preorder M]
[covariant_class M M has_mul.mul has_lt.lt]
{n : ℕ}
{x : M}
(hn : 0 < n)
(h : x < 1) :
theorem
right.pow_lt_one_of_lt
{M : Type u_4}
[monoid M]
[preorder M]
[covariant_class M M (function.swap has_mul.mul) has_lt.lt]
{n : ℕ}
{x : M}
(hn : 0 < n)
(h : x < 1) :
theorem
right.pow_neg
{M : Type u_4}
[add_monoid M]
[preorder M]
[covariant_class M M (function.swap has_add.add) has_lt.lt]
{n : ℕ}
{x : M}
(hn : 0 < n)
(h : x < 0) :
theorem
nsmul_nonneg_iff
{M : Type u_4}
[add_monoid M]
[linear_order M]
[covariant_class M M has_add.add has_le.le]
{x : M}
{n : ℕ}
(hn : n ≠ 0) :
theorem
one_le_pow_iff
{M : Type u_4}
[monoid M]
[linear_order M]
[covariant_class M M has_mul.mul has_le.le]
{x : M}
{n : ℕ}
(hn : n ≠ 0) :
theorem
nsmul_nonpos_iff
{M : Type u_4}
[add_monoid M]
[linear_order M]
[covariant_class M M has_add.add has_le.le]
{x : M}
{n : ℕ}
(hn : n ≠ 0) :
theorem
pow_le_one_iff
{M : Type u_4}
[monoid M]
[linear_order M]
[covariant_class M M has_mul.mul has_le.le]
{x : M}
{n : ℕ}
(hn : n ≠ 0) :
theorem
one_lt_pow_iff
{M : Type u_4}
[monoid M]
[linear_order M]
[covariant_class M M has_mul.mul has_le.le]
{x : M}
{n : ℕ}
(hn : n ≠ 0) :
theorem
nsmul_pos_iff
{M : Type u_4}
[add_monoid M]
[linear_order M]
[covariant_class M M has_add.add has_le.le]
{x : M}
{n : ℕ}
(hn : n ≠ 0) :
theorem
pow_lt_one_iff
{M : Type u_4}
[monoid M]
[linear_order M]
[covariant_class M M has_mul.mul has_le.le]
{x : M}
{n : ℕ}
(hn : n ≠ 0) :
theorem
nsmul_neg_iff
{M : Type u_4}
[add_monoid M]
[linear_order M]
[covariant_class M M has_add.add has_le.le]
{x : M}
{n : ℕ}
(hn : n ≠ 0) :
theorem
pow_eq_one_iff
{M : Type u_4}
[monoid M]
[linear_order M]
[covariant_class M M has_mul.mul has_le.le]
{x : M}
{n : ℕ}
(hn : n ≠ 0) :
theorem
nsmul_eq_zero_iff
{M : Type u_4}
[add_monoid M]
[linear_order M]
[covariant_class M M has_add.add has_le.le]
{x : M}
{n : ℕ}
(hn : n ≠ 0) :
theorem
nsmul_le_nsmul_iff
{M : Type u_4}
[add_monoid M]
[linear_order M]
[covariant_class M M has_add.add has_le.le]
[covariant_class M M has_add.add has_lt.lt]
{a : M}
{m n : ℕ}
(ha : 0 < a) :
theorem
pow_le_pow_iff'
{M : Type u_4}
[monoid M]
[linear_order M]
[covariant_class M M has_mul.mul has_le.le]
[covariant_class M M has_mul.mul has_lt.lt]
{a : M}
{m n : ℕ}
(ha : 1 < a) :
theorem
nsmul_lt_nsmul_iff
{M : Type u_4}
[add_monoid M]
[linear_order M]
[covariant_class M M has_add.add has_le.le]
[covariant_class M M has_add.add has_lt.lt]
{a : M}
{m n : ℕ}
(ha : 0 < a) :
theorem
pow_lt_pow_iff'
{M : Type u_4}
[monoid M]
[linear_order M]
[covariant_class M M has_mul.mul has_le.le]
[covariant_class M M has_mul.mul has_lt.lt]
{a : M}
{m n : ℕ}
(ha : 1 < a) :
theorem
lt_of_nsmul_lt_nsmul
{M : Type u_4}
[add_monoid M]
[linear_order 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}
(n : ℕ) :
theorem
lt_of_pow_lt_pow'
{M : Type u_4}
[monoid M]
[linear_order 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}
(n : ℕ) :
theorem
min_lt_max_of_mul_lt_mul
{M : Type u_4}
[monoid M]
[linear_order 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 c d : M}
(h : a * b < c * d) :
linear_order.min a b < linear_order.max c d
theorem
min_lt_max_of_add_lt_add
{M : Type u_4}
[add_monoid M]
[linear_order 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 c d : M}
(h : a + b < c + d) :
linear_order.min a b < linear_order.max c d
theorem
min_lt_of_mul_lt_sq
{M : Type u_4}
[monoid M]
[linear_order 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 c : M}
(h : a * b < c ^ 2) :
linear_order.min a b < c
theorem
min_lt_of_add_lt_two_nsmul
{M : Type u_4}
[add_monoid M]
[linear_order 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 c : M}
(h : a + b < 2 • c) :
linear_order.min a b < c
theorem
lt_max_of_sq_lt_mul
{M : Type u_4}
[monoid M]
[linear_order 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 c : M}
(h : a ^ 2 < b * c) :
a < linear_order.max b c
theorem
lt_max_of_two_nsmul_lt_add
{M : Type u_4}
[add_monoid M]
[linear_order 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 c : M}
(h : 2 • a < b + c) :
a < linear_order.max b c
theorem
le_of_pow_le_pow'
{M : Type u_4}
[monoid M]
[linear_order M]
[covariant_class M M has_mul.mul has_lt.lt]
[covariant_class M M (function.swap has_mul.mul) has_lt.lt]
{a b : M}
{n : ℕ}
(hn : n ≠ 0) :
theorem
le_of_nsmul_le_nsmul
{M : Type u_4}
[add_monoid M]
[linear_order M]
[covariant_class M M has_add.add has_lt.lt]
[covariant_class M M (function.swap has_add.add) has_lt.lt]
{a b : M}
{n : ℕ}
(hn : n ≠ 0) :
theorem
min_le_of_mul_le_sq
{M : Type u_4}
[monoid M]
[linear_order M]
[covariant_class M M has_mul.mul has_lt.lt]
[covariant_class M M (function.swap has_mul.mul) has_lt.lt]
{a b c : M}
(h : a * b ≤ c ^ 2) :
linear_order.min a b ≤ c
theorem
min_le_of_add_le_two_nsmul
{M : Type u_4}
[add_monoid M]
[linear_order M]
[covariant_class M M has_add.add has_lt.lt]
[covariant_class M M (function.swap has_add.add) has_lt.lt]
{a b c : M}
(h : a + b ≤ 2 • c) :
linear_order.min a b ≤ c
theorem
le_max_of_two_nsmul_le_add
{M : Type u_4}
[add_monoid M]
[linear_order M]
[covariant_class M M has_add.add has_lt.lt]
[covariant_class M M (function.swap has_add.add) has_lt.lt]
{a b c : M}
(h : 2 • a ≤ b + c) :
a ≤ linear_order.max b c
theorem
le_max_of_sq_le_mul
{M : Type u_4}
[monoid M]
[linear_order M]
[covariant_class M M has_mul.mul has_lt.lt]
[covariant_class M M (function.swap has_mul.mul) has_lt.lt]
{a b c : M}
(h : a ^ 2 ≤ b * c) :
a ≤ linear_order.max b c
theorem
left.nsmul_neg_iff
{M : Type u_4}
[add_monoid M]
[linear_order M]
[covariant_class M M has_add.add has_lt.lt]
{n : ℕ}
{x : M}
(hn : 0 < n) :
theorem
left.pow_lt_one_iff
{M : Type u_4}
[monoid M]
[linear_order M]
[covariant_class M M has_mul.mul has_lt.lt]
{n : ℕ}
{x : M}
(hn : 0 < n) :
theorem
right.pow_lt_one_iff
{M : Type u_4}
[monoid M]
[linear_order M]
[covariant_class M M (function.swap has_mul.mul) has_lt.lt]
{n : ℕ}
{x : M}
(hn : 0 < n) :
theorem
right.nsmul_neg_iff
{M : Type u_4}
[add_monoid M]
[linear_order M]
[covariant_class M M (function.swap has_add.add) has_lt.lt]
{n : ℕ}
{x : M}
(hn : 0 < n) :
theorem
one_le_zpow
{G : Type u_3}
[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) :
theorem
zsmul_nonneg
{G : Type u_3}
[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) :
theorem
canonically_ordered_comm_semiring.pow_pos
{R : Type u_5}
[canonically_ordered_comm_semiring R]
{a : R}
(H : 0 < a)
(n : ℕ) :
theorem
pow_lt_one
{R : Type u_5}
[ordered_semiring R]
{a : R}
(h₀ : 0 ≤ a)
(h₁ : a < 1)
{n : ℕ}
(hn : n ≠ 0) :
theorem
pow_le_pow_of_le_left
{R : Type u_5}
[ordered_semiring R]
{a b : R}
(ha : 0 ≤ a)
(hab : a ≤ b)
(i : ℕ) :
theorem
strict_mono_on_pow
{R : Type u_5}
[strict_ordered_semiring R]
{n : ℕ}
(hn : 0 < n) :
strict_mono_on (λ (x : R), x ^ n) (set.Ici 0)
theorem
pow_strict_mono_right
{R : Type u_5}
[strict_ordered_semiring R]
{a : R}
(h : 1 < a) :
strict_mono (λ (n : ℕ), a ^ n)
theorem
pow_lt_pow
{R : Type u_5}
[strict_ordered_semiring R]
{a : R}
{n m : ℕ}
(h : 1 < a)
(h2 : n < m) :
theorem
strict_anti_pow
{R : Type u_5}
[strict_ordered_semiring R]
{a : R}
(h₀ : 0 < a)
(h₁ : a < 1) :
strict_anti (λ (n : ℕ), a ^ n)
theorem
pow_lt_self_of_lt_one
{R : Type u_5}
[strict_ordered_semiring R]
{a : R}
{n : ℕ}
(h₀ : 0 < a)
(h₁ : a < 1)
(hn : 1 < n) :
theorem
lt_of_pow_lt_pow
{R : Type u_5}
[linear_ordered_semiring R]
{a b : R}
(n : ℕ)
(hb : 0 ≤ b)
(h : a ^ n < b ^ n) :
a < b
theorem
lt_of_mul_self_lt_mul_self
{R : Type u_5}
[linear_ordered_semiring R]
{a b : R}
(hb : 0 ≤ b) :
Alias of sq_nonneg.
Alias of sq_pos_of_ne_zero.
@[simp]
@[simp]
@[simp]
@[simp]
theorem
pow_four_le_pow_two_of_pow_two_le
{R : Type u_5}
[linear_ordered_ring R]
{x y : R}
(h : x ^ 2 ≤ y) :
Arithmetic mean-geometric mean (AM-GM) inequality for linearly ordered commutative rings.
Alias of two_mul_le_add_sq.
theorem
pow_pos_iff
{M : Type u_4}
[linear_ordered_comm_monoid_with_zero M]
[no_zero_divisors M]
{a : M}
{n : ℕ}
(hn : 0 < n) :
theorem
pow_lt_pow_succ
{M : Type u_4}
[linear_ordered_comm_group_with_zero M]
{a : M}
{n : ℕ}
(ha : 1 < a) :
theorem
pow_lt_pow₀
{M : Type u_4}
[linear_ordered_comm_group_with_zero M]
{a : M}
{m n : ℕ}
(ha : 1 < a)
(hmn : m < n) :
theorem
monoid_hom.map_neg_one
{M : Type u_4}
{R : Type u_5}
[ring R]
[monoid M]
[linear_order M]
[covariant_class M M has_mul.mul has_le.le]
(f : R →* M) :
@[simp]
theorem
monoid_hom.map_neg
{M : Type u_4}
{R : Type u_5}
[ring R]
[monoid M]
[linear_order M]
[covariant_class M M has_mul.mul has_le.le]
(f : R →* M)
(x : R) :
theorem
monoid_hom.map_sub_swap
{M : Type u_4}
{R : Type u_5}
[ring R]
[monoid M]
[linear_order M]
[covariant_class M M has_mul.mul has_le.le]
(f : R →* M)
(x y : R) :