Init.Data.Int.Pow

Int.pow_zero theorem

(b : Int) : b ^ 0 = 1

Full source

@[simp] protected theorem pow_zero (b : Int) : b^0 = 1 := rfl

Integer Power Zero Identity: $b^0 = 1$

Informal description

For any integer $b$, raising $b$ to the power of $0$ yields $1$, i.e., $b^0 = 1$.

Int.pow_succ theorem

(b : Int) (e : Nat) : b ^ (e + 1) = (b ^ e) * b

Full source

protected theorem pow_succ (b : Int) (e : Nat) : b ^ (e+1) = (b ^ e) * b := rfl

Integer Power Successor Identity: $b^{e+1} = b^e \cdot b$

Informal description

For any integer $b$ and natural number $e$, the power $b^{e+1}$ is equal to $b^e \cdot b$.

Int.pow_succ' theorem

(b : Int) (e : Nat) : b ^ (e + 1) = b * (b ^ e)

Full source

protected theorem pow_succ' (b : Int) (e : Nat) : b ^ (e+1) = b * (b ^ e) := by
  rw [Int.mul_comm, Int.pow_succ]

Integer Power Successor Identity (Alternate Form): $b^{e+1} = b \cdot b^e$

Informal description

For any integer $b$ and natural number $e$, the power $b^{e+1}$ is equal to $b$ multiplied by $b^e$, i.e., $b^{e+1} = b \cdot b^e$.

Int.pow_pos theorem

{n : Int} {m : Nat} : 0 < n → 0 < n ^ m

Full source

protected theorem pow_pos {n : Int} {m : Nat} : 0 < n → 0 < n ^ m := by
  induction m with
  | zero => simp
  | succ m ih => exact fun h => Int.mul_pos (ih h) h

Positivity of Integer Powers: $0 < n \implies 0 < n^m$

Informal description

For any integer $n$ and natural number $m$, if $0 < n$, then $0 < n^m$.

Int.pow_nonneg theorem

{n : Int} {m : Nat} : 0 ≤ n → 0 ≤ n ^ m

Full source

protected theorem pow_nonneg {n : Int} {m : Nat} : 0 ≤ n → 0 ≤ n ^ m := by
  induction m with
  | zero => simp
  | succ m ih => exact fun h => Int.mul_nonneg (ih h) h

Nonnegativity of Integer Powers: $0 \leq n \implies 0 \leq n^m$

Informal description

For any integer $n$ and natural number $m$, if $n$ is nonnegative (i.e., $0 \leq n$), then $n^m$ is also nonnegative (i.e., $0 \leq n^m$).

Int.pow_le_pow_of_le_left abbrev

Full source

@[deprecated Nat.pow_le_pow_left (since := "2025-02-17")]
abbrev pow_le_pow_of_le_left := @Nat.pow_le_pow_left

Exponentiation Preserves Order in Integers: $a \leq b \implies a^n \leq b^n$

Informal description

For any integers $a$ and $b$ such that $a \leq b$, and for any natural number $n$, it holds that $a^n \leq b^n$.

Int.pow_le_pow_of_le_right abbrev

Full source

@[deprecated Nat.pow_le_pow_right (since := "2025-02-17")]
abbrev pow_le_pow_of_le_right := @Nat.pow_le_pow_right

Monotonicity of Integer Powers: $a \geq 1 \land m \leq n \Rightarrow a^m \leq a^n$

Informal description

For any integer $a$ and natural numbers $m, n$ such that $m \leq n$, it holds that $a^m \leq a^n$ provided that $a \geq 1$.

Int.pos_pow_of_pos abbrev

Full source

@[deprecated Nat.pow_pos (since := "2025-02-17")]
abbrev pos_pow_of_pos := @Nat.pow_pos

Positivity of Integer Powers: $a > 0 \implies a^n > 0$

Informal description

For any integer $a > 0$ and natural number $n$, the power $a^n$ is also positive, i.e., $a^n > 0$.

Int.natCast_pow theorem

(b n : Nat) : ((b ^ n : Nat) : Int) = (b : Int) ^ n

Full source

@[norm_cast]
protected theorem natCast_pow (b n : Nat) : ((b^n : Nat) : Int) = (b : Int) ^ n := by
  match n with
  | 0 => rfl
  | n + 1 =>
    simp only [Nat.pow_succ, Int.pow_succ, Int.natCast_mul, Int.natCast_pow _ n]

Power Preservation under Natural-to-Integer Cast: $(b^n : \mathbb{N}) = (b : \mathbb{Z})^n$

Informal description

For any natural numbers $b$ and $n$, the canonical homomorphism from natural numbers to integers maps the power $b^n$ to the power of the image of $b$, i.e., $(b^n : \mathbb{N}) = (b : \mathbb{Z})^n$.

Int.two_pow_pred_sub_two_pow theorem

{w : Nat} (h : 0 < w) : ((2 ^ (w - 1) : Nat) - (2 ^ w : Nat) : Int) = -((2 ^ (w - 1) : Nat) : Int)

Full source

@[simp]
protected theorem two_pow_pred_sub_two_pow {w : Nat} (h : 0 < w) :
    ((2 ^ (w - 1) : Nat) - (2 ^ w : Nat) : Int) = - ((2 ^ (w - 1) : Nat) : Int) := by
  rw [← Nat.two_pow_pred_add_two_pow_pred h]
  omega

Integer Cast of Difference of Powers of Two: $(2^{w-1} - 2^w) = -2^{w-1}$ for $w > 0$

Informal description

For any natural number $w$ such that $w > 0$, the integer obtained by casting the natural number $2^{w-1} - 2^w$ equals the negation of the cast of $2^{w-1}$, i.e., $(2^{w-1} - 2^w : \mathbb{N}) = - (2^{w-1} : \mathbb{N})$ in $\mathbb{Z}$.

Int.two_pow_pred_sub_two_pow' theorem

{w : Nat} (h : 0 < w) : (2 : Int) ^ (w - 1) - (2 : Int) ^ w = -(2 : Int) ^ (w - 1)

Full source

@[simp]
protected theorem two_pow_pred_sub_two_pow' {w : Nat} (h : 0 < w) :
    (2 : Int) ^ (w - 1) - (2 : Int) ^ w = - (2 : Int) ^ (w - 1) := by
  norm_cast
  rw [← Nat.two_pow_pred_add_two_pow_pred h]
  simp [h]

Integer Power Difference Identity: $(2^{w-1} - 2^w) = -2^{w-1}$ for $w > 0$

Informal description

For any natural number $w$ such that $w > 0$, the difference of powers $(2 : \mathbb{Z})^{w-1} - (2 : \mathbb{Z})^w$ equals $-(2 : \mathbb{Z})^{w-1}$.