Commit 2023-10-09 15:23 fff0bc67

View on Github →

feat: prove equality of Nat.bitwise and Nat.bitwise' (#7410) This PR proves that Nat.bitwise (from core) and Nat.bitwise' (from mathlib) are equal

Estimated changes

Modified Mathlib/Data/Int/Bitwise.lean

Modified Mathlib/Data/Nat/Bitwise.lean

added theorem Nat.bitwise'_bit'

added theorem Nat.bitwise'_eq_bitwise

added theorem Nat.bitwise'_of_ne_zero

added theorem Nat.bitwise'_swap

added theorem Nat.bitwise'_zero_right

added theorem Nat.bitwise_bit

added theorem Nat.bitwise_of_ne_zero

added theorem Nat.bitwise_zero

added theorem Nat.bitwise_zero_left

added theorem Nat.bitwise_zero_right

added theorem Nat.land'_eq_land

added theorem Nat.land_bit

added theorem Nat.lor'_eq_lor

added theorem Nat.lor_bit

added theorem Nat.lxor_bit

added theorem Nat.xor'_eq_xor

Modified Mathlib/Data/Num/Lemmas.lean

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

deleted theorem Nat.bitwise'_swap

deleted theorem Nat.bitwise'_zero_right