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.

@[simp]
theorem ring_hom.map_fpow {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
@[simp]
theorem fpow_bit0_neg {K : Type u_1} [division_ring K] (x : K) (n : ) :
(-x) ^ bit0 n = x ^ bit0 n
theorem fpow_even_neg {K : Type u_1} [division_ring K] (a : K) {n : } (h : even n) :
(-a) ^ n = a ^ n
@[simp]
theorem fpow_bit1_neg {K : Type u_1} [division_ring K] (x : K) (n : ) :
(-x) ^ bit1 n = -x ^ bit1 n
theorem fpow_eq_zero_iff {K : Type u} [linear_ordered_field K] {a : K} {n : } (hn : 0 < n) :
a ^ n = 0 a = 0
theorem fpow_nonneg {K : Type u} [linear_ordered_field K] {a : K} (ha : 0 a) (z : ) :
0 a ^ z
theorem fpow_pos_of_pos {K : Type u} [linear_ordered_field K] {a : K} (ha : 0 < a) (z : ) :
0 < a ^ z
theorem fpow_le_of_le {K : Type u} [linear_ordered_field K] {x : K} (hx : 1 x) {a b : } (h : a b) :
x ^ a x ^ b
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)
theorem fpow_le_one_of_nonpos {K : Type u} [linear_ordered_field K] {p : K} (hp : 1 p) {z : } (hz : z 0) :
p ^ z 1
theorem one_le_fpow_of_nonneg {K : Type u} [linear_ordered_field K] {p : K} (hp : 1 p) {z : } (hz : 0 z) :
1 p ^ z
theorem fpow_bit0_nonneg {K : Type u} [linear_ordered_field K] (a : K) (n : ) :
0 a ^ bit0 n
theorem fpow_two_nonneg {K : Type u} [linear_ordered_field K] (a : K) :
0 a ^ 2
theorem fpow_bit0_pos {K : Type u} [linear_ordered_field K] {a : K} (h : a 0) (n : ) :
0 < a ^ bit0 n
theorem fpow_two_pos_of_ne_zero {K : Type u} [linear_ordered_field K] (a : K) (h : a 0) :
0 < a ^ 2
@[simp]
theorem fpow_bit1_neg_iff {K : Type u} [linear_ordered_field K] {a : K} {n : } :
a ^ bit1 n < 0 a < 0
@[simp]
theorem fpow_bit1_nonneg_iff {K : Type u} [linear_ordered_field K] {a : K} {n : } :
0 a ^ bit1 n 0 a
@[simp]
theorem fpow_bit1_nonpos_iff {K : Type u} [linear_ordered_field K] {a : K} {n : } :
a ^ bit1 n 0 a 0
@[simp]
theorem fpow_bit1_pos_iff {K : Type u} [linear_ordered_field K] {a : K} {n : } :
0 < a ^ bit1 n 0 < a
theorem fpow_even_nonneg {K : Type u} [linear_ordered_field K] (a : K) {n : } (hn : even n) :
0 a ^ n
theorem fpow_even_pos {K : Type u} [linear_ordered_field K] {a : K} {n : } (ha : a 0) (hn : even n) :
0 < a ^ n
theorem fpow_odd_nonneg {K : Type u} [linear_ordered_field K] {a : K} {n : } (ha : 0 a) (hn : odd n) :
0 a ^ n
theorem fpow_odd_pos {K : Type u} [linear_ordered_field K] {a : K} {n : } (ha : 0 < a) (hn : odd n) :
0 < a ^ n
theorem fpow_odd_nonpos {K : Type u} [linear_ordered_field K] {a : K} {n : } (ha : a 0) (hn : odd n) :
a ^ n 0
theorem fpow_odd_neg {K : Type u} [linear_ordered_field K] {a : K} {n : } (ha : a < 0) (hn : odd n) :
a ^ n < 0
theorem fpow_even_abs {K : Type u} [linear_ordered_field K] (a : K) {p : } (hp : even p) :
abs a ^ p = a ^ p
@[simp]
theorem fpow_bit0_abs {K : Type u} [linear_ordered_field K] (a : K) (p : ) :
abs a ^ bit0 p = a ^ bit0 p
theorem abs_fpow_even {K : Type u} [linear_ordered_field K] (a : K) {p : } (hp : even p) :
abs (a ^ p) = a ^ p
@[simp]
theorem abs_fpow_bit0 {K : Type u} [linear_ordered_field K] (a : K) (p : ) :
abs (a ^ bit0 p) = a ^ bit0 p
theorem one_lt_pow {K : Type u_1} [linear_ordered_semiring K] {p : K} (hp : 1 < p) {n : } :
1 n1 < p ^ n
theorem one_lt_fpow {K : Type u_1} [linear_ordered_field K] {p : K} (hp : 1 < p) (z : ) :
0 < z1 < p ^ z
theorem nat.fpow_pos_of_pos {K : Type u_1} [linear_ordered_field K] {p : } (h : 0 < p) (n : ) :
0 < p ^ n
theorem nat.fpow_ne_zero_of_pos {K : Type u_1} [linear_ordered_field K] {p : } (h : 0 < p) (n : ) :
p ^ n 0
theorem fpow_strict_mono {K : Type u_1} [linear_ordered_field K] {x : K} (hx : 1 < x) :
strict_mono (λ (n : ), x ^ n)
@[simp]
theorem fpow_lt_iff_lt {K : Type u_1} [linear_ordered_field K] {x : K} (hx : 1 < x) {m n : } :
x ^ m < x ^ n m < n
@[simp]
theorem fpow_le_iff_le {K : Type u_1} [linear_ordered_field K] {x : K} (hx : 1 < x) {m n : } :
x ^ m x ^ n m n
@[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
@[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
theorem fpow_injective {K : Type u_1} [linear_ordered_field K] {x : K} (h₀ : 0 < x) (h₁ : x 1) :
@[simp]
theorem fpow_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
@[simp]
theorem rat.cast_fpow {K : Type u_1} [field K] [char_zero K] (q : ) (n : ) :
(q ^ n) = q ^ n