Documentation Verification Report

BitIndices

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

Statistics

Metric	Count
Definitions `bitIndices`	1
Theorems `bitIndices_bit_false`, `bitIndices_bit_true`, `bitIndices_nodup`, `bitIndices_one`, `bitIndices_sorted`, `bitIndices_twoPowsum`, `bitIndices_two_mul`, `bitIndices_two_mul_add_one`, `bitIndices_two_pow`, `bitIndices_two_pow_mul`, `bitIndices_zero`, `notMem_bitIndices_self`, `twoPowSum_bitIndices`, `two_pow_le_of_mem_bitIndices`	14
Total	15

Nat

Definitions

Name	Category	Theorems
`bitIndices` 📖	CompOp	16 math math: `bitIndices_sorted`, `Finset.equivBitIndices_apply`, `Finset.toFinset_bitIndices_twoPowSum`, `bitIndices_one`, `twoPowSum_bitIndices`, `bitIndices_two_mul_add_one`, `bitIndices_zero`, `Finset.twoPowSum_toFinset_bitIndices`, `bitIndices_nodup`, `notMem_bitIndices_self`, `bitIndices_two_mul`, `bitIndices_two_pow_mul`, `bitIndices_bit_true`, `bitIndices_two_pow`, `bitIndices_twoPowsum`, `bitIndices_bit_false`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bitIndices_bit_false` 📖	mathematical	—	`bitIndices` `bit`	—	`binaryRec_eq`
`bitIndices_bit_true` 📖	mathematical	—	`bitIndices` `bit`	—	`binaryRec_eq`
`bitIndices_nodup` 📖	mathematical	—	`bitIndices`	—	`List.Pairwise.nodup` `instIrreflLt` `List.SortedLT.pairwise` `bitIndices_sorted`
`bitIndices_one` 📖	mathematical	—	`bitIndices`	—	—
`bitIndices_sorted` 📖	mathematical	—	`List.SortedLT` `instPreorder` `bitIndices`	—	`bitIndices_zero` `List.SortedLT.pairwise` `bitIndices_two_mul` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `bitIndices_two_mul_add_one` `instCanonicallyOrderedAdd`
`bitIndices_twoPowsum` 📖	mathematical	`List.SortedLT` `instPreorder`	`bitIndices` `MulZeroClass.toZero` `instMulZeroClass` `Monoid.toNatPow` `instMonoid`	—	—
`bitIndices_two_mul` 📖	mathematical	—	`bitIndices`	—	`bitIndices_bit_false` `bit_false`
`bitIndices_two_mul_add_one` 📖	mathematical	—	`bitIndices`	—	`bitIndices_bit_true` `bit_true`
`bitIndices_two_pow` 📖	mathematical	—	`bitIndices` `Monoid.toNatPow` `instMonoid`	—	`mul_one` `bitIndices_two_pow_mul` `bitIndices_one` `zero_add`
`bitIndices_two_pow_mul` 📖	mathematical	—	`bitIndices` `Monoid.toNatPow` `instMonoid`	—	`pow_zero` `one_mul` `add_zero` `add_comm` `pow_add` `pow_one` `mul_assoc` `bitIndices_two_mul` `comp_add_right`
`bitIndices_zero` 📖	mathematical	—	`bitIndices`	—	—
`notMem_bitIndices_self` 📖	mathematical	—	`bitIndices`	—	`LT.lt.not_ge` `two_pow_le_of_mem_bitIndices`
`twoPowSum_bitIndices` 📖	mathematical	—	`MulZeroClass.toZero` `instMulZeroClass` `Monoid.toNatPow` `instMonoid` `bitIndices`	—	`bitIndices_zero` `pow_add` `pow_one` `mul_comm` `bitIndices_two_mul` `List.sum_map_mul_left` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `instCharZero` `instAtLeastTwoHAddOfNat` `bitIndices_two_mul_add_one` `pow_zero` `add_comm`
`two_pow_le_of_mem_bitIndices` 📖	mathematical	`bitIndices`	`Monoid.toNatPow` `instMonoid`	—	`twoPowSum_bitIndices` `List.single_le_sum` `instIsOrderedAddMonoid` `instCanonicallyOrderedAdd`

---

← Back to Index