Theorems · Theorem · number theory

Num.castNum_eq_bitwise

∀ {f : Num → Num → Num} {g : Bool → Bool → Bool} (p : PosNum → PosNum → Num),
  g false false = false →
    f 0 0 = 0 →
      (∀ (n : PosNum), f 0 (Num.pos n) = bif g false true then Num.pos n else 0) →
        (∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0) →
          (∀ (m n : PosNum), f (Num.pos m) (Num.pos n) = p m n) →
            (p 1 1 = bif g true true then 1 else 0) →
              (∀ (b : Bool) (n : PosNum),
                  p 1 (PosNum.bit b n) = Num.bit (g true b) (bif g false true then Num.pos n else 0)) →
                (∀ (a : Bool) (m : PosNum),
                    p (PosNum.bit a m) 1 = Num.bit (g a true) (bif g true false then Num.pos m else 0)) →
                  (∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = Num.bit (g a b) (p m n)) →
                    ∀ (m n : Num), ↑(f m n) = Nat.bitwise g ↑m ↑n

Defined in

Mathlib.Data.Num.Lemmas

Cited by

4 results in Mathlib

Foundations

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