Documentation

Init.Data.Nat.Power2

theorem Nat.nextPowerOfTwo_dec {n power : Nat} (h₁ : power > 0) (h₂ : power < n) :
n - power * 2 < n - power
@[irreducible]
def Nat.nextPowerOfTwo.go (n power : Nat) (h : power > 0) :
Equations
@[irreducible]
theorem Nat.isPowerOfTwo_nextPowerOfTwo.isPowerOfTwo_go (n power : Nat) (h₁ : power > 0) (h₂ : power.isPowerOfTwo) :