Commit 2022-12-21 04:42 0c2d4344

View on Github →

feat: port Data.Nat.Bits (#1095) New Pull Request for data.nat.bits Reasons for opening:

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/EuclideanDomain/Defs.lean

Created Mathlib/Data/Nat/Bits.lean

added def Nat.binaryRec'

added def Nat.binaryRecFromOne

added theorem Nat.binary_rec_eq'

added theorem Nat.bit0_bits

added theorem Nat.bit0_eq_bit0

added theorem Nat.bit0_mod_two

added theorem Nat.bit1_bits

added theorem Nat.bit1_eq_bit1

added theorem Nat.bit1_eq_one

added theorem Nat.bit1_mod_two

added theorem Nat.bitCasesOn_bit0

added theorem Nat.bitCasesOn_bit1

added theorem Nat.bitCasesOn_bit

added theorem Nat.bit_add'

added theorem Nat.bit_add

added theorem Nat.bit_cases_on_inj

added theorem Nat.bit_cases_on_injective

added theorem Nat.bit_eq_zero_iff

added theorem Nat.bit_ne_zero

added theorem Nat.bits_append_bit

added theorem Nat.boddDiv2_eq

added theorem Nat.bodd_bit0

added theorem Nat.bodd_bit1

added theorem Nat.bodd_eq_bits_head

added theorem Nat.div2_bit0

added theorem Nat.div2_bit1

added theorem Nat.div2_bits_eq_tail

added theorem Nat.one_bits

added theorem Nat.one_eq_bit1

added theorem Nat.pos_of_bit0_pos

added theorem Nat.zero_bits

Modified Mathlib/Init/Align.lean

Modified Mathlib/Init/Data/List/Basic.lean

added def List.headI

Created Mathlib/Init/Data/Nat/Bitwise.lean

added def Nat.binaryRec

added theorem Nat.binaryRec_decreasing

added theorem Nat.binary_rec_eq

added theorem Nat.binary_rec_zero

added theorem Nat.bit0_val

added theorem Nat.bit1_val

added def Nat.bit

added def Nat.bitCasesOn

added theorem Nat.bit_decomp

added theorem Nat.bit_val

added theorem Nat.bit_zero

added def Nat.bits

added def Nat.bitwise'

added theorem Nat.bitwise'_bit

added theorem Nat.bitwise'_bit_aux

added theorem Nat.bitwise'_swap

added theorem Nat.bitwise'_zero

added theorem Nat.bitwise'_zero_left

added theorem Nat.bitwise'_zero_right

added def Nat.bodd

added def Nat.boddDiv2

added theorem Nat.bodd_add

added theorem Nat.bodd_add_div2

added theorem Nat.bodd_bit

added theorem Nat.bodd_mul

added theorem Nat.bodd_one

added theorem Nat.bodd_succ

added theorem Nat.bodd_two

added theorem Nat.bodd_zero

added def Nat.div2

added theorem Nat.div2_bit

added theorem Nat.div2_one

added theorem Nat.div2_succ

added theorem Nat.div2_two

added theorem Nat.div2_val

added theorem Nat.div2_zero

added def Nat.land'

added theorem Nat.land'_bit

added def Nat.ldiff'

added theorem Nat.ldiff'_bit

added def Nat.lor'

added theorem Nat.lor'_bit

added def Nat.lxor'

added theorem Nat.lxor'_bit

added theorem Nat.mod_two_of_bodd

added def Nat.shiftl'

added theorem Nat.shiftl'_add

added theorem Nat.shiftl'_sub

added def Nat.shiftl

added theorem Nat.shiftl_add

added theorem Nat.shiftl_sub

added theorem Nat.shiftl_succ

added theorem Nat.shiftl_zero

added def Nat.shiftr

added theorem Nat.shiftr_add

added theorem Nat.shiftr_zero

added def Nat.size

added def Nat.testBit

added theorem Nat.test_bit_bitwise'

added theorem Nat.test_bit_land'

added theorem Nat.test_bit_ldiff'

added theorem Nat.test_bit_lor'

added theorem Nat.test_bit_lxor'

added theorem Nat.test_bit_succ

added theorem Nat.test_bit_zero

Modified Mathlib/Init/Data/Nat/Lemmas.lean

Modified scripts/nolints.json