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

@[irreducible]

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

Nat

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

source

@[irreducible]

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

(nextPowerOfTwo.go n power h₁).isPowerOfTwo