HepLean Documentation

Init.Data.Int.Pow

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
theorem Int.pow_le_pow_of_le_left {n m : Nat} (h : n m) (i : Nat) :
n ^ i m ^ i
theorem Int.pow_le_pow_of_le_right {n : Nat} (hx : n > 0) {i j : Nat} :
i jn ^ i n ^ j
theorem Int.pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) :
0 < n ^ m
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)