Commit 2026-05-16 00:41 ca17ce0c

View on Github →

feat: add Nat.mem_bitIndices lemma and fix naming of surrounding lemmas (#39426) This PR adds the lemmas Nat.mem_bitIndices, relating Nat.bitIndices with Nat.testBit and indirectly via Nat.testBit_eq_inth and Nat.digits_two_eq_bits with Nat.bits and Nat.digits. Additionally, the naming of some lemmas is fixed to say sum_(map)?_*_two_pow instead of the nonexistent twoPowSum.

Estimated changes

Modified Mathlib/Combinatorics/Colex.lean

added theorem Finset.sum_toFinset_bitIndices_two_pow

added theorem Finset.toFinset_bitIndices_sum_two_pow

deleted theorem Finset.toFinset_bitIndices_twoPowSum

deleted theorem Finset.twoPowSum_toFinset_bitIndices

Modified Mathlib/Data/Nat/BitIndices.lean

added theorem Nat.bitIndices_sum_map_two_pow

deleted theorem Nat.bitIndices_twoPowsum

added theorem Nat.mem_bitIndices

added theorem Nat.sum_map_two_pow_bitIndices

deleted theorem Nat.twoPowSum_bitIndices

modified theorem Nat.two_pow_le_of_mem_bitIndices