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:

- `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✝

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

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

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

- Nat.one_isPowerOfTwo = Nat.isPowerOfTwo_one

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

- @Nat.mul2_isPowerOfTwo_of_isPowerOfTwo = @Nat.isPowerOfTwo_mul_two_of_isPowerOfTwo

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