Documentation Verification Report

BinaryRec

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

Statistics

MetricCount
DefinitionsbinaryRec, binaryRec', binaryRecFromOne, bit, bitCasesOn
5
TheoremsbinaryRec'_eq, binaryRec'_one, binaryRec'_zero, binaryRecFromOne_eq, binaryRecFromOne_one, binaryRecFromOne_zero, binaryRec_eq, binaryRec_one, binaryRec_zero, bitCasesOn_bit, bit_decide_mod_two_eq_one_shiftRight_one, bit_div_two, bit_eq_zero_iff, bit_false, bit_false_apply, bit_lt_two_pow_succ_iff, bit_mod_two, bit_ne_zero_iff, bit_shiftRight_one, bit_testBit_zero_shiftRight_one, bit_true, bit_true_apply, bit_val, log2_eq_succ_log2_shiftRight, shiftRight_one, testBit_bit_zero
26
Total31

Nat

Definitions

NameCategoryTheorems
binaryRec 📖CompOp
5 mathmath: binaryRec_zero, binaryRec_of_ne_zero, bitwise_eq_binaryRec, binaryRec_one, binaryRec_eq
binaryRec' 📖CompOp
3 mathmath: binaryRec'_zero, binaryRec'_one, binaryRec'_eq
binaryRecFromOne 📖CompOp
3 mathmath: binaryRecFromOne_one, binaryRecFromOne_eq, binaryRecFromOne_zero
bit 📖CompOp
54 mathmath: land_bit, bodd_bit, fast_fib_aux_bit_ff, div2_bit, bit_add, bitCasesOn_bit, bit_eq_zero_iff, log_two_bit, bit_decomp, bitwise_of_ne_zero, bit_true, Int.bit_negSucc, bit_true_apply, bit_bodd_div2, lor_bit, xor_bit, bit_mod_two_eq_one_iff, bit_mod_two, PosNum.bit_to_nat, fast_fib_aux_bit_tt, binaryRecFromOne_eq, Int.bit_coe_nat, Num.ofNat'_bit, size_bit, bit_false, bit_le, bits_append_bit, fastFibAux_bit_false, bit_div_two, Num.bit_to_nat, bit_decide_mod_two_eq_one_shiftRight_one, testBit_bit_zero, testBit_bit_succ, bit_val, binaryRec_of_ne_zero, bitwise_bit', bit_false_zero, bit_false_apply, bitwise_eq_binaryRec, bit_lt_bit, bit_lt_two_pow_succ_iff, bit_mod_two_eq_zero_iff, bit_shiftRight_one, bit_testBit_zero_shiftRight_one, bit_add', binaryRec'_eq, bitIndices_bit_true, fastFibAux_bit_true, ldiff_bit, bitIndices_bit_false, Equiv.boolProdNatEquivNat_apply, binaryRec_eq, bit_zero, bitwise_bit
bitCasesOn 📖CompOp
5 mathmath: bit_cases_on_injective, bitCasesOn_bit0, bitCasesOn_bit, bit_cases_on_inj, bitCasesOn_bit1

Theorems

NameKindAssumesProvesValidatesDepends On
binaryRec'_eq 📖mathematicalbinaryRec'
bit
binaryRec'.eq_1
binaryRec_eq
binaryRec'_one 📖mathematicalbinaryRec'binaryRec'.eq_1
binaryRec_one
binaryRec'_zero 📖mathematicalbinaryRec'binaryRec'.eq_1
binaryRec_zero
binaryRecFromOne_eq 📖mathematicalbinaryRecFromOne
bit
binaryRecFromOne.eq_1
binaryRec'_eq
binaryRecFromOne_one 📖mathematicalbinaryRecFromOnebinaryRecFromOne.eq_1
binaryRec'_one
binaryRecFromOne_zero 📖mathematicalbinaryRecFromOnebinaryRec'_zero
binaryRec_eq 📖mathematicalbinaryRec
bit
bit_eq_zero_iff
binaryRec.eq_def
binaryRec.eq_1
testBit_bit_zero
bit_shiftRight_one
bit_testBit_zero_shiftRight_one
binaryRec_one 📖mathematicalbinaryRec
binaryRec_zero 📖mathematicalbinaryRec
bitCasesOn_bit 📖mathematicalbitCasesOn
bit
testBit_bit_zero
bit_shiftRight_one
bit_testBit_zero_shiftRight_one
bit_decide_mod_two_eq_one_shiftRight_one 📖mathematicalbit
bit_div_two 📖mathematicalbitbit_val
bit_eq_zero_iff 📖mathematicalbit
bit_false 📖mathematicalbit
bit_false_apply 📖mathematicalbit
bit_lt_two_pow_succ_iff 📖mathematicalbit
bit_mod_two 📖mathematicalbitbit_val
bit_ne_zero_iff 📖
bit_shiftRight_one 📖mathematicalbitbit_div_two
bit_testBit_zero_shiftRight_one 📖mathematicalbitbit_decide_mod_two_eq_one_shiftRight_one
bit_true 📖mathematicalbit
bit_true_apply 📖mathematicalbit
bit_val 📖mathematicalbit
log2_eq_succ_log2_shiftRight 📖
shiftRight_one 📖
testBit_bit_zero 📖mathematicalbitbit_mod_two

---

← Back to Index