Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-01 01:14 cc20a865

View on Github →

feat(data/nat/basic): simp lemmas about inequalities with bit* (#2207)

  • feat(data/nat/basic): simp lemmas about inequalities with bit*
  • Fix compile of computability/partrec_code
  • Fix nat.bit_cases to work for Type* too
  • Generalize some lemmas to linear_ordered_semirings
  • Apply suggestions from code review Co-Authored-By: Gabriel Ebner [email protected]
  • Apply suggestions from code review Co-Authored-By: Scott Morrison [email protected]
  • fixing a proof

Estimated changes

added theorem bit0_le_bit0
added theorem bit0_lt_bit0
added theorem bit1_le_bit1
added theorem bit1_lt_bit1
added theorem one_le_bit1
added theorem one_lt_bit1
added theorem zero_le_bit0
added theorem zero_le_mul_left
added theorem zero_le_mul_right
added theorem zero_lt_bit0
added theorem zero_lt_mul_left
added theorem zero_lt_mul_right
added theorem nat.bit0_le_bit1_iff
added theorem nat.bit0_lt_bit1_iff
added theorem nat.bit1_le_bit0_iff
added theorem nat.bit1_lt_bit0_iff
added def nat.bit_cases
added theorem nat.bit_le_bit1_iff
added theorem nat.bit_le_bit_iff
added theorem nat.bit_lt_bit_iff
added theorem nat.one_le_bit0_iff
added theorem nat.one_lt_bit0_iff