Documentation

Init.Data.Nat.Power2

source
theorem Nat.nextPowerOfTwo_dec {n power : Nat} (h₁ : power > 0) (h₂ : power < n) :
n - power * 2 < n - power
source
def Nat.nextPowerOfTwo (n : Nat) :
Nat

Returns the least power of two that's greater than or equal to n.

Examples:

Equations
Instances For
    source
    def Nat.isPowerOfTwo (n : Nat) :
    Prop

    A natural number n is a power of two if there exists some k : Nat such that n = 2 ^ k.

    Equations
    Instances For
      source
      theorem Nat.isPowerOfTwo_one :
      isPowerOfTwo 1
      source
      @[reducible, inline, deprecated Nat.isPowerOfTwo_one (since := "2025-03-18")]
      abbrev Nat.one_isPowerOfTwo :
      isPowerOfTwo 1
      Equations
      Instances For
        source
        theorem Nat.isPowerOfTwo_mul_two_of_isPowerOfTwo {n : Nat} (h : n.isPowerOfTwo) :
        (n * 2).isPowerOfTwo
        source
        @[reducible, inline, deprecated Nat.isPowerOfTwo_mul_two_of_isPowerOfTwo (since := "2025-04-04")]
        abbrev Nat.mul2_isPowerOfTwo_of_isPowerOfTwo {n : Nat} (h : n.isPowerOfTwo) :
        (n * 2).isPowerOfTwo
        Equations
        Instances For
          source
          theorem Nat.pos_of_isPowerOfTwo {n : Nat} (h : n.isPowerOfTwo) :
          n > 0
          source
          theorem Nat.isPowerOfTwo_nextPowerOfTwo (n : Nat) :
          n.nextPowerOfTwo.isPowerOfTwo