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

def Nat.nextPowerOfTwo (n : Nat) : Nat

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

Examples:

• Nat.nextPowerOfTwo 0 = 1
• Nat.nextPowerOfTwo 1 = 1
• Nat.nextPowerOfTwo 2 = 2
• Nat.nextPowerOfTwo 3 = 4
• Nat.nextPowerOfTwo 5 = 8

Equations

• n.nextPowerOfTwo = Nat.nextPowerOfTwo.go n 1 Nat.nextPowerOfTwo.proof_1

@[irreducible]

def Nat.nextPowerOfTwo.go (n power : Nat) (h : power > 0) : Nat

Equations

• Nat.nextPowerOfTwo.go n power h = if power < n then Nat.nextPowerOfTwo.go n (power * 2) ⋯ else power

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

• n.isPowerOfTwo = ∃ (k : Nat), n = 2 ^ k

theorem Nat.isPowerOfTwo_one : isPowerOfTwo 1

@[reducible, inline, deprecated Nat.isPowerOfTwo_one (since := "2025-03-18")]

abbrev Nat.one_isPowerOfTwo : isPowerOfTwo 1

Equations

• Nat.one_isPowerOfTwo = Nat.isPowerOfTwo_one

theorem Nat.mul2_isPowerOfTwo_of_isPowerOfTwo {n : Nat} (h : n.isPowerOfTwo) : (n * 2).isPowerOfTwo

theorem Nat.pos_of_isPowerOfTwo {n : Nat} (h : n.isPowerOfTwo) : n > 0

theorem Nat.isPowerOfTwo_nextPowerOfTwo (n : Nat) : n.nextPowerOfTwo.isPowerOfTwo

@[irreducible]

theorem Nat.isPowerOfTwo_nextPowerOfTwo.isPowerOfTwo_go (n power : Nat) (h₁ : power > 0) (h₂ : power.isPowerOfTwo) : (nextPowerOfTwo.go n power h₁).isPowerOfTwo