Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-29 15:59 ba41f0a4

View on Github →

feat(data/nat): API for test_bit and bitwise operations (#3964)

Estimated changes

Modified src/data/bool.lean

added theorem bool.bxor_ff_left

added theorem bool.bxor_ff_right

Modified src/data/nat/basic.lean

deleted theorem nat.bitwise_comm

deleted theorem nat.land_comm

deleted theorem nat.lor_comm

deleted theorem nat.lxor_comm

Created src/data/nat/bitwise.lean

added theorem nat.bit_ff

added theorem nat.bit_tt

added theorem nat.bitwise_comm

added theorem nat.eq_of_test_bit_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_of_test_bit

added theorem nat.lxor_assoc

added theorem nat.lxor_comm

added theorem nat.lxor_eq_zero

added theorem nat.lxor_left_inj

added theorem nat.lxor_right_inj

added theorem nat.lxor_self

added theorem nat.lxor_zero

added theorem nat.zero_land

added theorem nat.zero_lor

added theorem nat.zero_lxor

added theorem nat.zero_of_test_bit_eq_ff

added theorem nat.zero_test_bit