Theorems · Theorem · number theory

PosNum.testBit.eq_def

∀ (x : PosNum) (x_1 : ℕ),
  x.testBit x_1 =
    match x, x_1 with
    | PosNum.one, 0 => true
    | PosNum.one, x => false
    | a.bit0, 0 => false
    | p.bit0, n.succ => p.testBit n
    | a.bit1, 0 => true
    | p.bit1, n.succ => p.testBit n

Defined in

Mathlib.Data.Num.Lemmas

Cited by

0 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms