Documentation

Init.Data.Int.Pow

pow #

@[simp]
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_pos {n : Int} {m : Nat} :
0 < n0 < n ^ m
theorem Int.pow_nonneg {n : Int} {m : Nat} :
0 n0 n ^ m
theorem Int.pow_ne_zero {n : Int} {m : Nat} :
n 0n ^ m 0
@[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
    Instances For
      @[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 jn ^ i n ^ j
      Equations
        Instances For
          @[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
            Instances For
              @[simp]
              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)
              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