Theorems · Theorem · number theory

Nat.bitwise_bit

∀ {f : Bool → Bool → Bool},
  autoParam (f false false = false) Nat.bitwise_bit._auto_1 →
    ∀ (a : Bool) (m : ℕ) (b : Bool) (n : ℕ),
      Nat.bitwise f (Nat.bit a m) (Nat.bit b n) = Nat.bit (f a b) (Nat.bitwise f m n)

Defined in

Mathlib.Data.Nat.Bitwise

Cited by

6 results in Mathlib

Foundations

Depth 31 from the axioms · uses propext, Classical.choice, Quot.sound