pow

theorem Int.pow_zero (b : Int) : b ^ 0 = 1

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

theorem Int.pow_succ' (b : Int) (e : Nat) : b ^ (e + 1) = b * b ^ e

@[reducible, inline, deprecated Nat.pow_le_pow_left (since := "2025-02-17")]

abbrev Int.pow_le_pow_of_le_left {n m : Nat} (h : n ≤ m) (i : Nat) : n ^ i ≤ m ^ i

Equations

• @Int.pow_le_pow_of_le_left = @Nat.pow_le_pow_left

@[reducible, inline, deprecated Nat.pow_le_pow_right (since := "2025-02-17")]

abbrev Int.pow_le_pow_of_le_right {n : Nat} (hx : n > 0) {i j : Nat} : i ≤ j → n ^ i ≤ n ^ j

Equations

• @Int.pow_le_pow_of_le_right = @Nat.pow_le_pow_right

@[reducible, inline, deprecated Nat.pow_pos (since := "2025-02-17")]

abbrev Int.pos_pow_of_pos {a n : Nat} (h : 0 < a) : 0 < a ^ n

Equations

• @Int.pos_pow_of_pos = @Nat.pow_pos

theorem Int.natCast_pow (b n : Nat) : ↑(b ^ n) = ↑b ^ n

@[simp]

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

@[simp]

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