Commit 2023-08-27 08:28 93bcc03c

View on Github →

chore: rename Nat.shiftl' to Nat.shiftLeft' (#6788) This makes it match the unprimed Nat.shiftLeft. Follows on from #6356 which removed Nat.shiftl.

Estimated changes

Modified Mathlib/Data/Int/Bitwise.lean

modified theorem Int.shiftl_negSucc

Modified Mathlib/Data/Nat/Bits.lean

Modified Mathlib/Data/Nat/Size.lean

added theorem Nat.shiftLeft'_ne_zero_left

added theorem Nat.shiftLeft'_tt_eq_mul_pow

added theorem Nat.shiftLeft'_tt_ne_zero

deleted theorem Nat.shiftl'_ne_zero_left

deleted theorem Nat.shiftl'_tt_eq_mul_pow

deleted theorem Nat.shiftl'_tt_ne_zero

added theorem Nat.size_shiftLeft'

deleted theorem Nat.size_shiftl'

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

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

added def Nat.shiftLeft'

added theorem Nat.shiftLeft'_add

added theorem Nat.shiftLeft'_false

added theorem Nat.shiftLeft'_sub

deleted def Nat.shiftl'

deleted theorem Nat.shiftl'_add

deleted theorem Nat.shiftl'_false

deleted theorem Nat.shiftl'_sub