Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-30 16:34 7ac96dea

View on Github →

refactor(data/nat/basic): move more bit theory out (#17763)

Estimated changes

Modified src/data/int/bitwise.lean

Modified src/data/nat/basic.lean

deleted theorem nat.bit0_eq_bit0

deleted theorem nat.bit0_mod_two

deleted theorem nat.bit1_eq_bit1

deleted theorem nat.bit1_eq_one

deleted theorem nat.bit1_mod_two

deleted theorem nat.bit_add'

deleted theorem nat.bit_add

deleted theorem nat.bit_cases_on_bit0

deleted theorem nat.bit_cases_on_bit1

deleted theorem nat.bit_cases_on_bit

deleted theorem nat.bit_cases_on_inj

deleted theorem nat.bit_cases_on_injective

deleted theorem nat.bit_ne_zero

deleted theorem nat.bodd_bit0

deleted theorem nat.bodd_bit1

deleted theorem nat.bodd_div2_eq

deleted theorem nat.div2_bit0

deleted theorem nat.div2_bit1

deleted theorem nat.one_eq_bit1

deleted theorem nat.pos_of_bit0_pos

Modified src/data/nat/bits.lean

added theorem nat.bit0_eq_bit0

added theorem nat.bit0_mod_two

added theorem nat.bit1_eq_bit1

added theorem nat.bit1_eq_one

added theorem nat.bit1_mod_two

added theorem nat.bit_add'

added theorem nat.bit_add

added theorem nat.bit_cases_on_bit0

added theorem nat.bit_cases_on_bit1

added theorem nat.bit_cases_on_bit

added theorem nat.bit_cases_on_inj

added theorem nat.bit_cases_on_injective

added theorem nat.bit_ne_zero

added theorem nat.bodd_bit0

added theorem nat.bodd_bit1

added theorem nat.bodd_div2_eq

added theorem nat.div2_bit0

added theorem nat.div2_bit1

added theorem nat.one_eq_bit1

added theorem nat.pos_of_bit0_pos

deleted theorem nat.size_eq_bits_len

Modified src/data/nat/bitwise.lean

Modified src/data/nat/pow.lean

deleted theorem nat.lt_size

deleted theorem nat.lt_size_self

deleted theorem nat.one_shiftl

deleted theorem nat.shiftl'_ne_zero_left

deleted theorem nat.shiftl'_tt_eq_mul_pow

deleted theorem nat.shiftl'_tt_ne_zero

deleted theorem nat.shiftl_eq_mul_pow

deleted theorem nat.shiftr_eq_div_pow

deleted theorem nat.size_bit0

deleted theorem nat.size_bit1

deleted theorem nat.size_bit

deleted theorem nat.size_eq_zero

deleted theorem nat.size_le

deleted theorem nat.size_le_size

deleted theorem nat.size_one

deleted theorem nat.size_pos

deleted theorem nat.size_pow

deleted theorem nat.size_shiftl'

deleted theorem nat.size_shiftl

deleted theorem nat.size_zero

deleted theorem nat.zero_shiftl

deleted theorem nat.zero_shiftr

Created src/data/nat/size.lean

added theorem nat.lt_size

added theorem nat.lt_size_self

added theorem nat.one_shiftl

added theorem nat.shiftl'_ne_zero_left

added theorem nat.shiftl'_tt_eq_mul_pow

added theorem nat.shiftl'_tt_ne_zero

added theorem nat.shiftl_eq_mul_pow

added theorem nat.shiftr_eq_div_pow

added theorem nat.size_bit0

added theorem nat.size_bit1

added theorem nat.size_bit

added theorem nat.size_eq_bits_len

added theorem nat.size_eq_zero

added theorem nat.size_le

added theorem nat.size_le_size

added theorem nat.size_one

added theorem nat.size_pos

added theorem nat.size_pow

added theorem nat.size_shiftl'

added theorem nat.size_shiftl

added theorem nat.size_zero

added theorem nat.zero_shiftl

added theorem nat.zero_shiftr

Modified src/data/nat/sqrt.lean

Modified src/data/num/lemmas.lean

Modified src/data/pnat/basic.lean