Documentation

Init.Data.Nat.Power2

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