Lemmas about the interaction of power operations with order #
Note that some lemmas are in Algebra/GroupPower/Lemmas.lean
as they import files which
depend on this file.
theorem
nsmul_le_nsmul_of_le_right
{M : Type u_1}
[inst : AddMonoid M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{a : M}
{b : M}
(hab : a ≤ b)
(i : ℕ)
:
Equations
- nsmul_le_nsmul_of_le_right.match_1 motive x h_1 h_2 = Nat.casesOn x (h_1 ()) fun n => h_2 n
theorem
pow_le_pow_of_le_left'
{M : Type u_1}
[inst : Monoid M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
{a : M}
{b : M}
(hab : a ≤ b)
(i : ℕ)
:
theorem
nsmul_lt_nsmul
{M : Type u_1}
[inst : AddMonoid M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
{a : M}
{n : ℕ}
{m : ℕ}
(ha : 0 < a)
(h : n < m)
:
theorem
nsmul_strictMono_right
{M : Type u_1}
[inst : AddMonoid M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
{a : M}
(ha : 0 < a)
:
StrictMono ((fun x x_1 => x_1 • x) a)
theorem
pow_strictMono_left
{M : Type u_1}
[inst : Monoid M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
{a : M}
(ha : 1 < a)
:
StrictMono ((fun x x_1 => x ^ x_1) a)
theorem
Right.pow_nonneg
{M : Type u_1}
[inst : AddMonoid M]
[inst : Preorder M]
[inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{x : M}
(hx : 0 ≤ x)
{n : ℕ}
:
theorem
Right.one_le_pow_of_le
{M : Type u_1}
[inst : Monoid M]
[inst : Preorder M]
[inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
{x : M}
(hx : 1 ≤ x)
{n : ℕ}
:
theorem
Right.pow_nonpos
{M : Type u_1}
[inst : AddMonoid M]
[inst : Preorder M]
[inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{x : M}
(hx : x ≤ 0)
{n : ℕ}
:
theorem
Right.pow_le_one_of_le
{M : Type u_1}
[inst : Monoid M]
[inst : Preorder M]
[inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
{x : M}
(hx : x ≤ 1)
{n : ℕ}
:
theorem
Right.pow_neg
{M : Type u_1}
[inst : AddMonoid M]
[inst : Preorder M]
[inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1]
{n : ℕ}
{x : M}
(hn : 0 < n)
(h : x < 0)
:
theorem
Right.pow_lt_one_of_lt
{M : Type u_1}
[inst : Monoid M]
[inst : Preorder M]
[inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1]
{n : ℕ}
{x : M}
(hn : 0 < n)
(h : x < 1)
:
theorem
nsmul_nonneg_iff
{M : Type u_1}
[inst : AddMonoid M]
[inst : LinearOrder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{x : M}
{n : ℕ}
(hn : n ≠ 0)
:
theorem
one_le_pow_iff
{M : Type u_1}
[inst : Monoid M]
[inst : LinearOrder M]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
{x : M}
{n : ℕ}
(hn : n ≠ 0)
:
theorem
nsmul_nonpos_iff
{M : Type u_1}
[inst : AddMonoid M]
[inst : LinearOrder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{x : M}
{n : ℕ}
(hn : n ≠ 0)
:
theorem
pow_le_one_iff
{M : Type u_1}
[inst : Monoid M]
[inst : LinearOrder M]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
{x : M}
{n : ℕ}
(hn : n ≠ 0)
:
theorem
nsmul_pos_iff
{M : Type u_1}
[inst : AddMonoid M]
[inst : LinearOrder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{x : M}
{n : ℕ}
(hn : n ≠ 0)
:
theorem
one_lt_pow_iff
{M : Type u_1}
[inst : Monoid M]
[inst : LinearOrder M]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
{x : M}
{n : ℕ}
(hn : n ≠ 0)
:
theorem
nsmul_neg_iff
{M : Type u_1}
[inst : AddMonoid M]
[inst : LinearOrder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{x : M}
{n : ℕ}
(hn : n ≠ 0)
:
theorem
pow_lt_one_iff
{M : Type u_1}
[inst : Monoid M]
[inst : LinearOrder M]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
{x : M}
{n : ℕ}
(hn : n ≠ 0)
:
theorem
nsmul_eq_zero_iff
{M : Type u_1}
[inst : AddMonoid M]
[inst : LinearOrder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{x : M}
{n : ℕ}
(hn : n ≠ 0)
:
theorem
pow_eq_one_iff
{M : Type u_1}
[inst : Monoid M]
[inst : LinearOrder M]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
{x : M}
{n : ℕ}
(hn : n ≠ 0)
:
theorem
nsmul_le_nsmul_iff
{M : Type u_1}
[inst : AddMonoid M]
[inst : LinearOrder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
{a : M}
{m : ℕ}
{n : ℕ}
(ha : 0 < a)
:
theorem
pow_le_pow_iff'
{M : Type u_1}
[inst : Monoid M]
[inst : LinearOrder M]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
{a : M}
{m : ℕ}
{n : ℕ}
(ha : 1 < a)
:
theorem
nsmul_lt_nsmul_iff
{M : Type u_1}
[inst : AddMonoid M]
[inst : LinearOrder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
{a : M}
{m : ℕ}
{n : ℕ}
(ha : 0 < a)
:
theorem
pow_lt_pow_iff'
{M : Type u_1}
[inst : Monoid M]
[inst : LinearOrder M]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
{a : M}
{m : ℕ}
{n : ℕ}
(ha : 1 < a)
:
theorem
Left.nsmul_neg_iff
{M : Type u_1}
[inst : AddMonoid M]
[inst : LinearOrder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
{n : ℕ}
{x : M}
(hn : 0 < n)
:
theorem
Left.pow_lt_one_iff'
{M : Type u_1}
[inst : Monoid M]
[inst : LinearOrder M]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
{n : ℕ}
{x : M}
(hn : 0 < n)
:
theorem
Left.pow_lt_one_iff
{M : Type u_1}
[inst : Monoid M]
[inst : LinearOrder M]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
{n : ℕ}
{x : M}
(hn : 0 < n)
:
theorem
Right.nsmul_neg_iff
{M : Type u_1}
[inst : AddMonoid M]
[inst : LinearOrder M]
[inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1]
{n : ℕ}
{x : M}
(hn : 0 < n)
:
theorem
Right.pow_lt_one_iff
{M : Type u_1}
[inst : Monoid M]
[inst : LinearOrder M]
[inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1]
{n : ℕ}
{x : M}
(hn : 0 < n)
:
theorem
zsmul_nonneg
{G : Type u_1}
[inst : SubNegMonoid G]
[inst : Preorder G]
[inst : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{x : G}
(H : 0 ≤ x)
{n : ℤ}
(hn : 0 ≤ n)
:
theorem
one_le_zpow
{G : Type u_1}
[inst : DivInvMonoid G]
[inst : Preorder G]
[inst : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
{x : G}
(H : 1 ≤ x)
{n : ℤ}
(hn : 0 ≤ n)
:
theorem
CanonicallyOrderedCommSemiring.pow_pos
{R : Type u_1}
[inst : CanonicallyOrderedCommSemiring R]
{a : R}
(H : 0 < a)
(n : ℕ)
:
theorem
one_le_pow_of_one_le
{R : Type u_1}
[inst : OrderedSemiring R]
{a : R}
(H : 1 ≤ a)
(n : ℕ)
:
theorem
le_self_pow
{R : Type u_1}
[inst : OrderedSemiring R]
{a : R}
{m : ℕ}
(ha : 1 ≤ a)
(h : m ≠ 0)
:
theorem
strictMonoOn_pow
{R : Type u_1}
[inst : StrictOrderedSemiring R]
{n : ℕ}
(hn : 0 < n)
:
StrictMonoOn (fun x => x ^ n) (Set.Ici 0)
theorem
strictMono_pow
{R : Type u_1}
[inst : StrictOrderedSemiring R]
{a : R}
(h : 1 < a)
:
StrictMono fun n => a ^ n
theorem
strictAnti_pow
{R : Type u_1}
[inst : StrictOrderedSemiring R]
{a : R}
(h₀ : 0 < a)
(h₁ : a < 1)
:
StrictAnti fun n => a ^ n
theorem
pow_bit0_pos_of_neg
{R : Type u_1}
[inst : StrictOrderedRing R]
{a : R}
(ha : a < 0)
(n : ℕ)
:
theorem
lt_of_mul_self_lt_mul_self
{R : Type u_1}
[inst : LinearOrderedSemiring R]
{a : R}
{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_1}
[inst : LinearOrderedRing R]
{x : R}
{y : R}
(h : x ^ 2 ≤ y)
:
Alias of two_mul_le_add_sq
.
theorem
pow_pos_iff
{M : Type u_1}
[inst : LinearOrderedCommMonoidWithZero M]
[inst : NoZeroDivisors M]
{a : M}
{n : ℕ}
(hn : 0 < n)
:
theorem
MonoidHom.map_neg_one
{M : Type u_1}
{R : Type u_2}
[inst : Ring R]
[inst : Monoid M]
[inst : LinearOrder M]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
(f : R →* M)
:
@[simp]
theorem
MonoidHom.map_neg
{M : Type u_1}
{R : Type u_2}
[inst : Ring R]
[inst : Monoid M]
[inst : LinearOrder M]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
(f : R →* M)
(x : R)
:
theorem
MonoidHom.map_sub_swap
{M : Type u_1}
{R : Type u_2}
[inst : Ring R]
[inst : Monoid M]
[inst : LinearOrder M]
[inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
(f : R →* M)
(x : R)
(y : R)
: