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 zpow_bit1_neg {α : Type u_1} [division_ring α] (x : α) (n : ) :
(-x) ^ bit1 n = -x ^ bit1 n
@[simp, norm_cast]
theorem rat.cast_zpow {α : Type u_1} [division_ring α] [char_zero α] (q : ) (n : ) :
(q ^ n) = q ^ n
theorem zpow_nonneg {α : Type u_1} [linear_ordered_semifield α] {a : α} (ha : 0 a) (z : ) :
0 a ^ z
theorem zpow_pos_of_pos {α : Type u_1} [linear_ordered_semifield α] {a : α} (ha : 0 < a) (z : ) :
0 < a ^ z
theorem zpow_le_of_le {α : Type u_1} [linear_ordered_semifield α] {a : α} {m n : } (ha : 1 a) (h : m n) :
a ^ m a ^ n
theorem pow_le_max_of_min_le {α : Type u_1} [linear_ordered_semifield α] {x : α} (hx : 1 x) {a b c : } (h : linear_order.min a b c) :
x ^ -c linear_order.max (x ^ -a) (x ^ -b)
theorem zpow_le_one_of_nonpos {α : Type u_1} [linear_ordered_semifield α] {a : α} {n : } (ha : 1 a) (hn : n 0) :
a ^ n 1
theorem one_le_zpow_of_nonneg {α : Type u_1} [linear_ordered_semifield α] {a : α} {n : } (ha : 1 a) (hn : 0 n) :
1 a ^ n
@[protected]
theorem nat.zpow_pos_of_pos {α : Type u_1} [linear_ordered_semifield α] {a : } (h : 0 < a) (n : ) :
0 < a ^ n
theorem nat.zpow_ne_zero_of_pos {α : Type u_1} [linear_ordered_semifield α] {a : } (h : 0 < a) (n : ) :
a ^ n 0
theorem one_lt_zpow {α : Type u_1} [linear_ordered_semifield α] {a : α} (ha : 1 < a) (n : ) :
0 < n1 < a ^ n
theorem zpow_strict_mono {α : Type u_1} [linear_ordered_semifield α] {x : α} (hx : 1 < x) :
theorem zpow_strict_anti {α : Type u_1} [linear_ordered_semifield α] {x : α} (h₀ : 0 < x) (h₁ : x < 1) :
@[simp]
theorem zpow_lt_iff_lt {α : Type u_1} [linear_ordered_semifield α] {x : α} {m n : } (hx : 1 < x) :
x ^ m < x ^ n m < n
@[simp]
theorem zpow_le_iff_le {α : Type u_1} [linear_ordered_semifield α] {x : α} {m n : } (hx : 1 < x) :
x ^ m x ^ n m n
theorem min_le_of_zpow_le_max {α : Type u_1} [linear_ordered_semifield α] {x : α} (hx : 1 < x) {a b c : } (h_max : x ^ -c linear_order.max (x ^ -a) (x ^ -b)) :
@[simp]
theorem pos_div_pow_pos {α : Type u_1} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (hb : 0 < b) (k : ) :
0 < a / b ^ k
@[simp]
theorem div_pow_le {α : Type u_1} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (hb : 1 b) (k : ) :
a / b ^ k a
theorem zpow_injective {α : Type u_1} [linear_ordered_semifield α] {x : α} (h₀ : 0 < x) (h₁ : x 1) :
@[simp]
theorem zpow_inj {α : Type u_1} [linear_ordered_semifield α] {x : α} {m n : } (h₀ : 0 < x) (h₁ : x 1) :
x ^ m = x ^ n m = n
theorem zpow_bit0_nonneg {α : Type u_1} [linear_ordered_field α] (a : α) (n : ) :
0 a ^ bit0 n
theorem zpow_two_nonneg {α : Type u_1} [linear_ordered_field α] (a : α) :
0 a ^ 2
theorem zpow_bit0_pos {α : Type u_1} [linear_ordered_field α] {a : α} (h : a 0) (n : ) :
0 < a ^ bit0 n
theorem zpow_two_pos_of_ne_zero {α : Type u_1} [linear_ordered_field α] {a : α} (h : a 0) :
0 < a ^ 2
@[simp]
theorem zpow_bit1_neg_iff {α : Type u_1} [linear_ordered_field α] {a : α} {n : } :
a ^ bit1 n < 0 a < 0
@[simp]
theorem zpow_bit1_nonneg_iff {α : Type u_1} [linear_ordered_field α] {a : α} {n : } :
0 a ^ bit1 n 0 a
@[simp]
theorem zpow_bit1_nonpos_iff {α : Type u_1} [linear_ordered_field α] {a : α} {n : } :
a ^ bit1 n 0 a 0
@[simp]
theorem zpow_bit1_pos_iff {α : Type u_1} [linear_ordered_field α] {a : α} {n : } :
0 < a ^ bit1 n 0 < a