# pow #

source
@[simp]
theorem Int.pow_zero (b : Int) :
b ^ 0 = 1
source
theorem Int.pow_succ (b : Int) (e : Nat) :
b ^ (e + 1) = b ^ e * b
source
theorem Int.pow_succ' (b : Int) (e : Nat) :
b ^ (e + 1) = b * b ^ e
source
theorem Int.pow_add (a : Int) (m n : Nat) :
a ^ (m + n) = a ^ m * a ^ n
source
theorem Int.zero_pow {n : Nat} (h : n ≠ 0) :
0 ^ n = 0
source
theorem Int.one_pow {n : Nat} :
1 ^ n = 1
source
theorem Int.pow_pos {n : Int} {m : Nat} :
0 < n → 0 < n ^ m
source
theorem Int.pow_nonneg {n : Int} {m : Nat} :
0 ≤ n → 0 ≤ n ^ m
source
theorem Int.pow_ne_zero {n : Int} {m : Nat} :
n ≠ 0 → n ^ m ≠ 0
source
instance Int.instNeZeroHPowNat {n : Int} {m : Nat} [NeZero n] :
NeZero (n ^ m)
source
@[reducible, inline, deprecated Nat.pow_pos (since := "2025-02-17")]
abbrev Nat.pos_pow_of_pos {a n : Nat} (h : 0 < a) :
0 < a ^ n
Equations

- @Nat.pos_pow_of_pos = @Nat.pow_pos

Instances For

source
@[simp]
theorem Int.natCast_pow (b n : Nat) :
↑(b ^ n) = ↑b ^ n
source
@[simp]
theorem Int.two_pow_pred_sub_two_pow {w : Nat} (h : 0 < w) :
↑(2 ^ (w - 1)) - ↑(2 ^ w) = -↑(2 ^ (w - 1))
source
@[simp]
theorem Int.two_pow_pred_sub_two_pow' {w : Nat} (h : 0 < w) :
2 ^ (w - 1) - 2 ^ w = -2 ^ (w - 1)
source
theorem Int.pow_lt_pow_of_lt {a : Int} {b c : Nat} (ha : 1 < a) (hbc : b < c) :
a ^ b < a ^ c
source
@[simp]
theorem Int.natAbs_pow (n : Int) (k : Nat) :
(n ^ k).natAbs = n.natAbs ^ k
source
theorem Int.toNat_pow_of_nonneg {x : Int} (h : 0 ≤ x) (k : Nat) :
(x ^ k).toNat = x.toNat ^ k