Theorems · Theorem · number theory

Nat.bitwise_eq_binaryRec

∀ (f : Bool → Bool → Bool),
  Nat.bitwise f = fun n =>
    Nat.binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
      (fun a m Ia n => Nat.binaryRec (bif f true false then Nat.bit a m else 0) (fun b n x => Nat.bit (f a b) (Ia n)) n)
      n

Defined in

Mathlib.Data.Nat.Bitwise

Cited by

0 results in Mathlib

Foundations

Depth 38 from the axioms · uses propext, Quot.sound