Bitwise

📁 Source: Mathlib/Data/Nat/Bitwise.lean

Statistics

Metric	Count
Definitions tacticBitwise_assoc_tac	1
Theorems and_two_pow, append_lt, binaryRec_of_ne_zero, bit_mod_two_eq_one_iff, bit_mod_two_eq_zero_iff, bitwise_bit, bitwise_bit', bitwise_comm, bitwise_eq_binaryRec, bitwise_of_ne_zero, bitwise_swap, bitwise_zero, bitwise_zero_left, bitwise_zero_right, even_xor, exists_most_significant_bit, land_assoc, land_bit, land_comm, ldiff_bit, lor_assoc, lor_bit, lor_comm, lt_of_testBit, lt_xor_cases, shiftLeft_lt, testBit_eq_false_of_lt, testBit_eq_inth, testBit_land, testBit_ldiff, testBit_lor, two_pow_and, xor_bit, xor_cancel_left, xor_cancel_right, xor_eq_zero, xor_mod_two_eq, xor_ne_zero, xor_one_of_even, xor_one_of_odd, xor_range, xor_trichotomy, zero_of_testBit_eq_false	43
Total	44

Nat

Definitions

Name	Category	Theorems
tacticBitwise_assoc_tac 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
and_two_pow 📖	mathematical	—	Monoid.toNatPow instMonoid	—	Decidable.eq_or_ne MulZeroClass.zero_mul one_mul
append_lt 📖	—	Monoid.toNatPow instMonoid	—	—	add_comm shiftLeft_lt lt_of_lt_of_le
binaryRec_of_ne_zero 📖	mathematical	—	binaryRec bit bodd div2 bit_bodd_div2	—	bit_bodd_div2 binaryRec_eq bodd_bit div2_bit
bit_mod_two_eq_one_iff 📖	mathematical	—	bit	—	bit_mod_two
bit_mod_two_eq_zero_iff 📖	mathematical	—	bit	—	bit_mod_two
bitwise_bit 📖	mathematical	—	bit	—	instAtLeastTwoHAddOfNat two_mul add_comm zero_add IsDomain.to_noZeroDivisors instIsDomain instCharZero mul_div_cancel_left₀ instMulDivCancelClass bitwise_zero_left MulZeroClass.mul_zero bitwise_zero_right
bitwise_bit' 📖	mathematical	—	bit	—	bit_ne_zero_iff div2_bit two_mul
bitwise_comm 📖	—	—	—	—	bitwise_swap
bitwise_eq_binaryRec 📖	mathematical	—	binaryRec bit	—	bitwise_zero_left bit_bodd_div2 binaryRec_of_ne_zero bit_ne_zero_iff bodd_bit div2_bit bitwise_zero_right bitwise_of_ne_zero
bitwise_of_ne_zero 📖	mathematical	—	bit bodd	—	mod_two_of_bodd two_mul
bitwise_swap 📖	mathematical	—	Function.swap	—	bitwise_zero_left bitwise_zero_right bitwise_of_ne_zero bodd_succ div_lt_self'
bitwise_zero 📖	—	—	—	—	bitwise_zero_right
bitwise_zero_left 📖	—	—	—	—	—
bitwise_zero_right 📖	—	—	—	—	—
even_xor 📖	mathematical	—	Even	—	xor_mod_two_eq
exists_most_significant_bit 📖	—	—	—	—	MulZeroClass.mul_zero zero_add testBit_bit_zero testBit_bit_succ
land_assoc 📖	—	—	—	—	land_bit
land_bit 📖	mathematical	—	bit	—	bitwise_bit
land_comm 📖	—	—	—	—	bitwise_comm
ldiff_bit 📖	mathematical	—	ldiff bit	—	bitwise_bit
lor_assoc 📖	—	—	—	—	lor_bit
lor_bit 📖	mathematical	—	bit	—	bitwise_bit
lor_comm 📖	—	—	—	—	bitwise_comm
lt_of_testBit 📖	—	—	—	—	testBit_bit_succ testBit_bit_zero bit_false bit_true bit_lt_bit
lt_xor_cases 📖	—	—	—	—	xor_trichotomy LT.lt.ne LT.lt.asymm
shiftLeft_lt 📖	—	Monoid.toNatPow instMonoid	—	—	—
testBit_eq_false_of_lt 📖	—	Monoid.toNatPow instMonoid	—	—	—
testBit_eq_inth 📖	mathematical	—	List.getI bits	—	mod_two_of_bodd bodd_eq_bits_head List.getI_zero_eq_headI bit_bodd_div2 testBit_bit_succ div2_bits_eq_tail
testBit_land 📖	—	—	—	—	—
testBit_ldiff 📖	mathematical	—	ldiff	—	—
testBit_lor 📖	—	—	—	—	—
two_pow_and 📖	mathematical	—	Monoid.toNatPow instMonoid	—	mul_comm land_comm and_two_pow
xor_bit 📖	mathematical	—	bit	—	bitwise_bit
xor_cancel_left 📖	—	—	—	—	—
xor_cancel_right 📖	—	—	—	—	—
xor_eq_zero 📖	—	—	—	—	—
xor_mod_two_eq 📖	—	—	—	—	—
xor_ne_zero 📖	—	—	—	—	—
xor_one_of_even 📖	—	Even	—	—	even_iff instAtLeastTwoHAddOfNat bitwise_zero_right div_two_mul_two_of_even
xor_one_of_odd 📖	—	Odd instSemiring	—	—	not_odd_zero bitwise_zero_right
xor_range 📖	—	—	—	—	zero_add xor_one_of_even even_iff
xor_trichotomy 📖	—	—	—	—	exists_most_significant_bit Mathlib.Tactic.Contrapose.contrapose₁ Bool.eq_false_eq_not_eq_true lt_of_testBit
zero_of_testBit_eq_false 📖	—	—	—	—	bit_mod_two bit_false testBit_bit_succ

---

← Back to Index