Commit 2022-12-21 06:53 dddfba93

View on Github →

feat: Port Data.Nat.Size (#1140) 550b58538991c8977703fdeb7c9d51a5aa27df11

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Nat/Order/Basic.lean

added theorem Nat.bit0_le_bit1_iff

added theorem Nat.bit0_le_bit

added theorem Nat.bit0_lt_bit1_iff

added theorem Nat.bit1_le_bit0_iff

added theorem Nat.bit1_lt_bit0_iff

added theorem Nat.bit_le

added theorem Nat.bit_le_bit1

added theorem Nat.bit_lt_bit0

added theorem Nat.bit_lt_bit

Created Mathlib/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