HepLean 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
Equations
Instances For
    @[irreducible]
    def Nat.nextPowerOfTwo.go (n : Nat) (power : Nat) (h : power > 0) :
    Equations
    Instances For
      Equations
      • n.isPowerOfTwo = ∃ (k : Nat), n = 2 ^ k
      Instances For
        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
        @[irreducible]
        theorem Nat.isPowerOfTwo_nextPowerOfTwo.isPowerOfTwo_go (n : Nat) (power : Nat) (h₁ : power > 0) (h₂ : power.isPowerOfTwo) :
        (Nat.nextPowerOfTwo.go n power h₁).isPowerOfTwo