Commit 2023-01-09 08:09 23f6bf24

View on Github →

feat: port Data.Nat.Bitwise (#1404) depends on

depends on: #1407
depends on: #1415 otherwise simp cannot unify past a panic would be nice:
leanprover/lean4#2017 will simplify bitwise_assoc_tac

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Bitwise.lean

added theorem Nat.bit_eq_zero

added theorem Nat.bit_false

added theorem Nat.bit_true

added theorem Nat.bitwise'_comm

added theorem Nat.eq_of_testBit_eq

added theorem Nat.exists_most_significant_bit

added theorem Nat.land'_assoc

added theorem Nat.land'_comm

added theorem Nat.land'_zero

added theorem Nat.lor'_assoc

added theorem Nat.lor'_comm

added theorem Nat.lor'_zero

added theorem Nat.lt_lxor'_cases

added theorem Nat.lt_of_testBit

added theorem Nat.lxor'_assoc

added theorem Nat.lxor'_cancel_left

added theorem Nat.lxor'_comm

added theorem Nat.lxor'_eq_zero

added theorem Nat.lxor'_left_inj

added theorem Nat.lxor'_left_injective

added theorem Nat.lxor'_ne_zero

added theorem Nat.lxor'_right_inj

added theorem Nat.lxor'_right_injective

added theorem Nat.lxor'_self

added theorem Nat.lxor'_trichotomy

added theorem Nat.lxor'_zero

added theorem Nat.lxor_cancel_right

added theorem Nat.testBit_eq_inth

added theorem Nat.testBit_two_pow

added theorem Nat.testBit_two_pow_of_ne

added theorem Nat.testBit_two_pow_self

added theorem Nat.zero_land'

added theorem Nat.zero_lor'

added theorem Nat.zero_lxor'

added theorem Nat.zero_of_testBit_eq_false

added theorem Nat.zero_testBit