Documentation

Init.Data.Nat.Power2

theorem Nat.two_pow_pos (w : Nat) :

0 < 2 ^ w

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

n - power * 2 < n - power

def Nat.nextPowerOfTwo (n : Nat) :

Equations

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

Instances For

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

Equations

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

Instances For

def Nat.isPowerOfTwo (n : Nat) :

Equations

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

Instances For

theorem Nat.one_isPowerOfTwo :

Nat.isPowerOfTwo 1

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

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

(Nat.nextPowerOfTwo.go n power h₁).isPowerOfTwo