Documentation

Mathlib.Algebra.Order.Field.Power

Lemmas about powers in ordered fields. #

source
theorem Even.zpow_nonneg {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {n : ℤ} (hn : Even n) (a : α) :
0 ≤ a ^ n
source
theorem zpow_two_nonneg {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a : α) :
0 ≤ a ^ 2
source
theorem zpow_neg_two_nonneg {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a : α) :
0 ≤ a ^ (-2)
source
theorem Even.zpow_pos {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} {n : ℤ} (hn : Even n) (ha : a ≠ 0) :
0 < a ^ n
source
theorem zpow_two_pos_of_ne_zero {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (ha : a ≠ 0) :
0 < a ^ 2
source
theorem Even.zpow_pos_iff {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} {n : ℤ} (hn : Even n) (h : n ≠ 0) :
0 < a ^ n ↔ a ≠ 0
source
theorem Odd.zpow_neg_iff {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} {n : ℤ} (hn : Odd n) :
a ^ n < 0 ↔ a < 0
source
theorem Odd.zpow_nonneg_iff {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} {n : ℤ} (hn : Odd n) :
0 ≤ a ^ n ↔ 0 ≤ a
source
theorem Odd.zpow_nonpos_iff {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} {n : ℤ} (hn : Odd n) :
a ^ n ≤ 0 ↔ a ≤ 0
source
theorem Odd.zpow_pos_iff {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} {n : ℤ} (hn : Odd n) :
0 < a ^ n ↔ 0 < a
source
theorem Odd.zpow_neg {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} {n : ℤ} (hn : Odd n) :
a < 0 → a ^ n < 0

Alias of the reverse direction of Odd.zpow_neg_iff.

source
theorem Odd.zpow_nonpos {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} {n : ℤ} (hn : Odd n) :
a ≤ 0 → a ^ n ≤ 0

Alias of the reverse direction of Odd.zpow_nonpos_iff.

source
theorem Even.zpow_abs {α : Type u_1} [Field α] [LinearOrder α] {p : ℤ} (hp : Even p) (a : α) :
|a| ^ p = a ^ p
source
theorem zpow_eq_zpow_iff_of_ne_zero₀ {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} {n : ℤ} (hn : n ≠ 0) :
a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n
source
theorem zpow_eq_zpow_iff_cases₀ {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} {n : ℤ} :
a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n
source
theorem zpow_eq_one_iff_of_ne_zero₀ {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} {n : ℤ} (hn : n ≠ 0) :
a ^ n = 1 ↔ a = 1 ∨ a = -1 ∧ Even n
source
theorem zpow_eq_one_iff_cases₀ {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} {n : ℤ} :
a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n
source
theorem zpow_eq_neg_zpow_iff₀ {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : α} {n : ℤ} (hb : b ≠ 0) :
a ^ n = -b ^ n ↔ a = -b ∧ Odd n
source
theorem zpow_eq_neg_one_iff₀ {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} {n : ℤ} :
a ^ n = -1 ↔ a = -1 ∧ Odd n

Bernoulli's inequality #

source
theorem Nat.cast_le_pow_sub_div_sub {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (H : 1 < a) (n : ℕ) :
↑n ≤ (a ^ n - 1) / (a - 1)

Bernoulli's inequality reformulated to estimate (n : α).

source
theorem Nat.cast_le_pow_div_sub {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (H : 1 < a) (n : ℕ) :
↑n ≤ a ^ n / (a - 1)

For any a > 1 and a natural n we have n ≤ a ^ n / (a - 1). See also Nat.cast_le_pow_sub_div_sub for a stronger inequality with a ^ n - 1 in the numerator.

source
def Mathlib.Meta.Positivity.evalZPow :
PositivityExt

The positivity extension which identifies expressions of the form a ^ (b : ℤ), such that positivity successfully recognises both a and b.

Equations
  • One or more equations did not get rendered due to their size.
Instances For