Commit 2023-09-10 18:23 83d7426b

View on Github →

refactor(Data/Int/Bitwise): use <<< and >>> notation (#6789) The lemma names have changed to use shiftLeft and shiftRight to match the new Nat names.

Estimated changes

Modified Mathlib/Data/Int/Bitwise.lean

added theorem Int.one_shiftLeft

deleted theorem Int.one_shiftl

added theorem Int.shiftLeft_add

added theorem Int.shiftLeft_coe_nat

added theorem Int.shiftLeft_eq_mul_pow

added theorem Int.shiftLeft_neg

added theorem Int.shiftLeft_negSucc

added theorem Int.shiftLeft_sub

added theorem Int.shiftRight_add

added theorem Int.shiftRight_coe_nat

added theorem Int.shiftRight_eq_div_pow

added theorem Int.shiftRight_neg

added theorem Int.shiftRight_negSucc

deleted theorem Int.shiftl_add

deleted theorem Int.shiftl_coe_nat

deleted theorem Int.shiftl_eq_mul_pow

deleted theorem Int.shiftl_neg

deleted theorem Int.shiftl_negSucc

deleted theorem Int.shiftl_sub

deleted theorem Int.shiftr_add

deleted theorem Int.shiftr_coe_nat

deleted theorem Int.shiftr_eq_div_pow

deleted theorem Int.shiftr_neg

deleted theorem Int.shiftr_negSucc

added theorem Int.zero_shiftLeft

added theorem Int.zero_shiftRight

deleted theorem Int.zero_shiftl

deleted theorem Int.zero_shiftr

Modified Mathlib/Init/Data/Int/Bitwise.lean

deleted def Int.shiftl

deleted def Int.shiftr