mathlib documentation

algebra.field_power

Integer power operation on fields and division rings #

This file collects basic facts about the operation of raising an element of a division_ring to an integer power. More specialised results are provided in the case of a linearly ordered field.

source
@[simp]
theorem ring_hom.map_zpow {K : Type u_1} {L : Type u_2} [division_ring K] [division_ring L] (f : K →+* L) (a : K) (n : ℤ) :
⇑f (a ^ n) = ⇑f a ^ n
source
@[simp]
theorem ring_equiv.map_zpow {K : Type u_1} {L : Type u_2} [division_ring K] [division_ring L] (f : K ≃+* L) (a : K) (n : ℤ) :
⇑f (a ^ n) = ⇑f a ^ n
source
@[simp]
theorem zpow_bit0_neg {K : Type u_1} [division_ring K] (x : K) (n : ℤ) :
(-x) ^ bit0 n = x ^ bit0 n
source
theorem even.zpow_neg {K : Type u_1} [division_ring K] {n : ℤ} (h : even n) (a : K) :
(-a) ^ n = a ^ n
source
@[simp]
theorem zpow_bit1_neg {K : Type u_1} [division_ring K] (x : K) (n : ℤ) :
(-x) ^ bit1 n = -x ^ bit1 n
source
theorem zpow_eq_zero_iff {K : Type u} [linear_ordered_field K] {a : K} {n : ℤ} (hn : 0 < n) :
a ^ n = 0 ↔ a = 0
source
theorem zpow_nonneg {K : Type u} [linear_ordered_field K] {a : K} (ha : 0 ≤ a) (z : ℤ) :
0 ≤ a ^ z
source
theorem zpow_pos_of_pos {K : Type u} [linear_ordered_field K] {a : K} (ha : 0 < a) (z : ℤ) :
0 < a ^ z
source
theorem zpow_le_of_le {K : Type u} [linear_ordered_field K] {x : K} (hx : 1 ≤ x) {a b : ℤ} (h : a ≤ b) :
x ^ a ≤ x ^ b
source
theorem pow_le_max_of_min_le {K : Type u} [linear_ordered_field K] {x : K} (hx : 1 ≤ x) {a b c : ℤ} (h : min a b ≤ c) :
x ^ -c ≤ max (x ^ -a) (x ^ -b)
source
theorem zpow_le_one_of_nonpos {K : Type u} [linear_ordered_field K] {p : K} (hp : 1 ≤ p) {z : ℤ} (hz : z ≤ 0) :
p ^ z ≤ 1
source
theorem one_le_zpow_of_nonneg {K : Type u} [linear_ordered_field K] {p : K} (hp : 1 ≤ p) {z : ℤ} (hz : 0 ≤ z) :
1 ≤ p ^ z
source
theorem zpow_bit0_nonneg {K : Type u} [linear_ordered_field K] (a : K) (n : ℤ) :
0 ≤ a ^ bit0 n
source
theorem zpow_two_nonneg {K : Type u} [linear_ordered_field K] (a : K) :
0 ≤ a ^ 2
source
theorem zpow_bit0_pos {K : Type u} [linear_ordered_field K] {a : K} (h : a ≠ 0) (n : ℤ) :
0 < a ^ bit0 n
source
theorem zpow_two_pos_of_ne_zero {K : Type u} [linear_ordered_field K] (a : K) (h : a ≠ 0) :
0 < a ^ 2
source
@[simp]
theorem zpow_bit1_neg_iff {K : Type u} [linear_ordered_field K] {a : K} {n : ℤ} :
a ^ bit1 n < 0 ↔ a < 0
source
@[simp]
theorem zpow_bit1_nonneg_iff {K : Type u} [linear_ordered_field K] {a : K} {n : ℤ} :
0 ≤ a ^ bit1 n ↔ 0 ≤ a
source
@[simp]
theorem zpow_bit1_nonpos_iff {K : Type u} [linear_ordered_field K] {a : K} {n : ℤ} :
a ^ bit1 n ≤ 0 ↔ a ≤ 0
source
@[simp]
theorem zpow_bit1_pos_iff {K : Type u} [linear_ordered_field K] {a : K} {n : ℤ} :
0 < a ^ bit1 n ↔ 0 < a
source
theorem even.zpow_nonneg {K : Type u} [linear_ordered_field K] {n : ℤ} (hn : even n) (a : K) :
0 ≤ a ^ n
source
theorem even.zpow_pos {K : Type u} [linear_ordered_field K] {a : K} {n : ℤ} (hn : even n) (ha : a ≠ 0) :
0 < a ^ n
source
theorem odd.zpow_nonneg {K : Type u} [linear_ordered_field K] {a : K} {n : ℤ} (hn : odd n) (ha : 0 ≤ a) :
0 ≤ a ^ n
source
theorem odd.zpow_pos {K : Type u} [linear_ordered_field K] {a : K} {n : ℤ} (hn : odd n) (ha : 0 < a) :
0 < a ^ n
source
theorem odd.zpow_nonpos {K : Type u} [linear_ordered_field K] {a : K} {n : ℤ} (hn : odd n) (ha : a ≤ 0) :
a ^ n ≤ 0
source
theorem odd.zpow_neg {K : Type u} [linear_ordered_field K] {a : K} {n : ℤ} (hn : odd n) (ha : a < 0) :
a ^ n < 0
source
theorem even.zpow_abs {K : Type u} [linear_ordered_field K] {p : ℤ} (hp : even p) (a : K) :
|a| ^ p = a ^ p
source
@[simp]
theorem zpow_bit0_abs {K : Type u} [linear_ordered_field K] (a : K) (p : ℤ) :
|a| ^ bit0 p = a ^ bit0 p
source
theorem even.abs_zpow {K : Type u} [linear_ordered_field K] {p : ℤ} (hp : even p) (a : K) :
|a ^ p| = a ^ p
source
@[simp]
theorem abs_zpow_bit0 {K : Type u} [linear_ordered_field K] (a : K) (p : ℤ) :
|a ^ bit0 p| = a ^ bit0 p
source
theorem one_lt_zpow {K : Type u_1} [linear_ordered_field K] {p : K} (hp : 1 < p) (z : ℤ) :
0 < z → 1 < p ^ z
source
theorem nat.zpow_pos_of_pos {K : Type u_1} [linear_ordered_field K] {p : ℕ} (h : 0 < p) (n : ℤ) :
0 < ↑p ^ n
source
theorem nat.zpow_ne_zero_of_pos {K : Type u_1} [linear_ordered_field K] {p : ℕ} (h : 0 < p) (n : ℤ) :
↑p ^ n ≠ 0
source
theorem zpow_strict_mono {K : Type u_1} [linear_ordered_field K] {x : K} (hx : 1 < x) :
strict_mono (λ (n : ℤ), x ^ n)
source
theorem zpow_strict_anti {K : Type u_1} [linear_ordered_field K] {x : K} (h₀ : 0 < x) (h₁ : x < 1) :
strict_anti (λ (n : ℤ), x ^ n)
source
@[simp]
theorem zpow_lt_iff_lt {K : Type u_1} [linear_ordered_field K] {x : K} (hx : 1 < x) {m n : ℤ} :
x ^ m < x ^ n ↔ m < n
source
@[simp]
theorem zpow_le_iff_le {K : Type u_1} [linear_ordered_field K] {x : K} (hx : 1 < x) {m n : ℤ} :
x ^ m ≤ x ^ n ↔ m ≤ n
source
@[simp]
theorem pos_div_pow_pos {K : Type u_1} [linear_ordered_field K] {a b : K} (ha : 0 < a) (hb : 0 < b) (k : ℕ) :
0 < a / b ^ k
source
@[simp]
theorem div_pow_le {K : Type u_1} [linear_ordered_field K] {a b : K} (ha : 0 < a) (hb : 1 ≤ b) (k : ℕ) :
a / b ^ k ≤ a
source
theorem zpow_injective {K : Type u_1} [linear_ordered_field K] {x : K} (h₀ : 0 < x) (h₁ : x ≠ 1) :
function.injective (pow x)
source
@[simp]
theorem zpow_inj {K : Type u_1} [linear_ordered_field K] {x : K} (h₀ : 0 < x) (h₁ : x ≠ 1) {m n : ℤ} :
x ^ m = x ^ n ↔ m = n
source
@[simp, norm_cast]
theorem rat.cast_zpow {K : Type u_1} [field K] [char_zero K] (q : ℚ) (n : ℤ) :
↑(q ^ n) = ↑q ^ n