Skip to content

Commit

Permalink
Update Bitwise.lean
Browse files Browse the repository at this point in the history
  • Loading branch information
pitmonticone committed Oct 20, 2024
1 parent ba27a19 commit 76e2b9e
Showing 1 changed file with 1 addition and 2 deletions.
3 changes: 1 addition & 2 deletions Mathlib/Data/Nat/Bitwise.lean
Original file line number Diff line number Diff line change
Expand Up @@ -366,8 +366,7 @@ theorem xor_mod_two_eq {m n : ℕ} : (m ^^^ n) % 2 = (m + n) % 2 := by
@[simp]
theorem even_xor {m n : ℕ} : Even (m ^^^ n) ↔ (Even m ↔ Even n) := by
simp only [even_iff, xor_mod_two_eq]
simp only [← even_iff]
exact even_add
omega

@[simp] theorem bit_lt_two_pow_succ_iff {b x n} : bit b x < 2 ^ (n + 1) ↔ x < 2 ^ n := by
cases b <;> simp <;> omega
Expand Down

0 comments on commit 76e2b9e

Please sign in to comment.