pow

@[simp]

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

theorem Int.negSucc_pow (m n : Nat) : negSucc m ^ n = if n % 2 = 0 then ofNat (m.succ ^ n) else negOfNat (m.succ ^ n)

@[simp]

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

theorem Int.pow_succ (m : Int) (n : Nat) : m ^ n.succ = m ^ n * m

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

theorem Int.pow_add (a : Int) (m n : Nat) : a ^ (m + n) = a ^ m * a ^ n

theorem Int.zero_pow {n : Nat} (h : n ≠ 0) : 0 ^ n = 0

theorem Int.one_pow {n : Nat} : 1 ^ n = 1

theorem Int.mul_pow {a b : Int} {n : Nat} : (a * b) ^ n = a ^ n * b ^ n

theorem Int.pow_one (a : Int) : a ^ 1 = a

theorem Int.pow_mul {a : Int} {n m : Nat} : a ^ (n * m) = (a ^ n) ^ m

theorem Int.pow_pos {n : Int} {m : Nat} : 0 < n → 0 < n ^ m

theorem Int.pow_nonneg {n : Int} {m : Nat} : 0 ≤ n → 0 ≤ n ^ m

theorem Int.pow_ne_zero {n : Int} {m : Nat} : n ≠ 0 → n ^ m ≠ 0

instance Int.instNeZeroHPowNat {n : Int} {m : Nat} [NeZero n] : NeZero (n ^ m)

instance Int.instNeZeroHPowOfNat {n : Int} : NeZero (n ^ 0)

@[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)

theorem Int.pow_lt_pow_of_lt {a : Int} {b c : Nat} (ha : 1 < a) (hbc : b < c) : a ^ b < a ^ c

@[simp]

theorem Int.natAbs_pow (n : Int) (k : Nat) : (n ^ k).natAbs = n.natAbs ^ k

theorem Int.toNat_pow_of_nonneg {x : Int} (h : 0 ≤ x) (k : Nat) : (x ^ k).toNat = x.toNat ^ k

theorem Int.sq_nonnneg (m : Int) : 0 ≤ m ^ 2

theorem Int.pow_nonneg_of_even {m : Int} {n : Nat} (h : n % 2 = 0) : 0 ≤ m ^ n

theorem Int.neg_pow {m : Int} {n : Nat} : (-m) ^ n = (-1) ^ (n % 2) * m ^ n