Bits

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

Statistics

Metric	Count
Definitions `bits`, `bodd`, `boddDiv2`, `div2`, `ldiff`, `shiftLeft'`, `size`	7
Theorems `binaryRec_decreasing`, `bit0_bits`, `bit1_bits`, `bitCasesOn_bit0`, `bitCasesOn_bit1`, `bit_add`, `bit_add'`, `bit_bodd_div2`, `bit_cases_on_inj`, `bit_cases_on_injective`, `bit_decomp`, `bit_false_zero`, `bit_le`, `bit_lt_bit`, `bit_ne_zero`, `bit_zero`, `bits_append_bit`, `boddDiv2_eq`, `bodd_add`, `bodd_add_div2`, `bodd_bit`, `bodd_eq_bits_head`, `bodd_eq_one_and_ne_zero`, `bodd_mul`, `bodd_one`, `bodd_succ`, `bodd_two`, `bodd_zero`, `div2_bit`, `div2_bit0`, `div2_bit1`, `div2_bits_eq_tail`, `div2_one`, `div2_succ`, `div2_two`, `div2_val`, `div2_zero`, `mod_two_of_bodd`, `one_bits`, `shiftLeft'_add`, `shiftLeft'_false`, `shiftLeft'_sub`, `shiftLeft_eq'`, `shiftLeft_sub`, `shiftRight_eq`, `testBit_bit_succ`, `zero_bits`	47
Total	54

Nat

Definitions

Name	Category	Theorems
`bits` 📖	CompOp	10 math math: `testBit_eq_inth`, `one_bits`, `size_eq_bits_len`, `bit1_bits`, `bits_append_bit`, `zero_bits`, `bodd_eq_bits_head`, `div2_bits_eq_tail`, `bit0_bits`, `digits_two_eq_bits`
`bodd` 📖	CompOp	20 math, 3 bridge math: `bodd_bit`, `bodd_mul`, `bit_decomp`, `bitwise_of_ne_zero`, `bit_bodd_div2`, `Int.bodd_negOfNat`, `Equiv.natSumNatEquivNat_symm_apply`, `Int.bodd_subNatNat`, `boddDiv2_eq`, `binaryRec_of_ne_zero`, `div2_succ`, `bodd_add`, `bodd_succ`, `bodd_eq_bits_head`, `bodd_eq_one_and_ne_zero`, `mod_two_of_bodd`, `bodd_add_div2`, `Computable.nat_bodd`, `Int.bodd_coe`, `Primrec.nat_bodd` bridge: `bodd_two`, `bodd_one`, `bodd_zero`
`boddDiv2` 📖	CompOp	2 math math: `boddDiv2_eq`, `Equiv.boolProdNatEquivNat_symm_apply`
`div2` 📖	CompOp	18 math math: `div2_bit`, `div2_two`, `bit_decomp`, `bit_bodd_div2`, `div2_zero`, `Equiv.natSumNatEquivNat_symm_apply`, `div2_val`, `binaryRec_decreasing`, `boddDiv2_eq`, `binaryRec_of_ne_zero`, `div2_succ`, `div2_bit0`, `Computable.nat_div2`, `Primrec.nat_div2`, `div2_bits_eq_tail`, `div2_one`, `div2_bit1`, `bodd_add_div2`
`ldiff` 📖	CompOp	3 math math: `testBit_ldiff`, `Num.castNum_ldiff`, `ldiff_bit`
`shiftLeft'` 📖	CompOp	6 math math: `shiftLeft'_false`, `size_shiftLeft'`, `shiftLeft'_sub`, `Int.shiftLeft_negSucc`, `shiftLeft'_add`, `shiftLeft'_tt_eq_mul_pow`
`size` 📖	CompOp	17 math math: `size_one`, `size_shiftLeft`, `PosNum.size_to_nat`, `Num.size_to_nat`, `size_shiftLeft'`, `size_zero`, `lt_size`, `lt_size_self`, `size_eq_bits_len`, `size_eq_zero`, `PosNum.natSize_to_nat`, `size_bit`, `size_le_size`, `Num.natSize_to_nat`, `size_pow`, `size_pos`, `size_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`binaryRec_decreasing` 📖	mathematical	—	`div2`	—	—
`bit0_bits` 📖	mathematical	—	`bits`	—	`bits_append_bit`
`bit1_bits` 📖	mathematical	—	`bits`	—	`bits_append_bit`
`bitCasesOn_bit0` 📖	mathematical	—	`bitCasesOn`	—	`bitCasesOn_bit`
`bitCasesOn_bit1` 📖	mathematical	—	`bitCasesOn`	—	`bitCasesOn_bit`
`bit_add` 📖	mathematical	—	`bit`	—	—
`bit_add'` 📖	mathematical	—	`bit`	—	—
`bit_bodd_div2` 📖	mathematical	—	`bit` `bodd` `div2`	—	`bit_val` `bodd_add_div2`
`bit_cases_on_inj` 📖	mathematical	—	`bitCasesOn`	—	`bit_cases_on_injective`
`bit_cases_on_injective` 📖	mathematical	—	`bitCasesOn`	—	`bitCasesOn_bit`
`bit_decomp` 📖	mathematical	—	`bit` `bodd` `div2`	—	`bit_bodd_div2`
`bit_false_zero` 📖	mathematical	—	`bit`	—	—
`bit_le` 📖	mathematical	—	`bit`	—	—
`bit_lt_bit` 📖	mathematical	—	`bit`	—	—
`bit_ne_zero` 📖	—	—	—	—	—
`bit_zero` 📖	mathematical	—	`bit`	—	`bit_false_zero`
`bits_append_bit` 📖	mathematical	—	`bits` `bit`	—	`bits.eq_1` `binaryRec_eq`
`boddDiv2_eq` 📖	mathematical	—	`boddDiv2` `bodd` `div2`	—	—
`bodd_add` 📖	mathematical	—	`bodd`	—	`bodd_succ`
`bodd_add_div2` 📖	mathematical	—	`bodd` `div2`	—	`bodd_succ` `div2_succ`
`bodd_bit` 📖	mathematical	—	`bodd` `bit`	—	`bit_val` `bodd_add` `bodd_mul` `bodd_succ`
`bodd_eq_bits_head` 📖	mathematical	—	`bodd` `List.headI` `bits`	—	`zero_bits` `bodd_bit` `bits_append_bit`
`bodd_eq_one_and_ne_zero` 📖	mathematical	—	`bodd`	—	`bodd_succ`
`bodd_mul` 📖	mathematical	—	`bodd`	—	`bodd_add` `bodd_succ`
`bodd_one` 📖	bridging (complete)	—	`bodd`	`bodd`	—
`bodd_succ` 📖	mathematical	—	`bodd`	—	—
`bodd_two` 📖	bridging (complete)	—	`bodd`	`bodd`	—
`bodd_zero` 📖	bridging (complete)	—	`bodd`	`bodd`	—
`div2_bit` 📖	mathematical	—	`div2` `bit`	—	`bit_val` `div2_val`
`div2_bit0` 📖	mathematical	—	`div2`	—	`div2_bit`
`div2_bit1` 📖	mathematical	—	`div2`	—	`div2_bit`
`div2_bits_eq_tail` 📖	mathematical	—	`bits` `div2`	—	`zero_bits` `div2_bit` `bits_append_bit`
`div2_one` 📖	mathematical	—	`div2`	—	—
`div2_succ` 📖	mathematical	—	`div2` `bodd`	—	—
`div2_two` 📖	mathematical	—	`div2`	—	—
`div2_val` 📖	mathematical	—	`div2`	—	`mod_two_of_bodd` `bodd_add_div2`
`div2_zero` 📖	mathematical	—	`div2`	—	—
`mod_two_of_bodd` 📖	mathematical	—	`bodd`	—	`bodd_add` `bodd_mul` `bodd_succ`
`one_bits` 📖	mathematical	—	`bits`	—	`bit1_bits`
`shiftLeft'_add` 📖	mathematical	—	`shiftLeft'`	—	—
`shiftLeft'_false` 📖	mathematical	—	`shiftLeft'`	—	`bit_val`
`shiftLeft'_sub` 📖	mathematical	—	`shiftLeft'`	—	`shiftLeft'.eq_2` `div2_bit`
`shiftLeft_eq'` 📖	—	—	—	—	—
`shiftLeft_sub` 📖	—	—	—	—	`shiftLeft'_sub`
`shiftRight_eq` 📖	—	—	—	—	—
`testBit_bit_succ` 📖	mathematical	—	`bit`	—	`div2_bit` `bodd_eq_one_and_ne_zero`
`zero_bits` 📖	mathematical	—	`bits`	—	—

---

← Back to Index