Skip to content

Commit

Permalink
Update Mathlib/Data/Nat/Bitwise.lean
Browse files Browse the repository at this point in the history
Co-authored-by: Eric Wieser <[email protected]>
  • Loading branch information
pitmonticone and eric-wieser authored Oct 20, 2024
1 parent 94e9c33 commit ba27a19
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Data/Nat/Bitwise.lean
Original file line number Diff line number Diff line change
Expand Up @@ -357,7 +357,7 @@ theorem lt_xor_cases {a b c : ℕ} (h : a < b ^^^ c) : a ^^^ c < b ∨ a ^^^ b <
theorem xor_mod_two_eq {m n : ℕ} : (m ^^^ n) % 2 = (m + n) % 2 := by
by_cases h : (m + n) % 2 = 0
· simp only [h, mod_two_eq_zero_iff_testBit_zero, testBit_zero, xor_mod_two_eq_one, decide_not,
Bool.decide_iff_dist, Bool.not_eq_false', beq_iff_eq, decide_eq_decide]
Bool.decide_iff_dist, Bool.not_eq_false', beq_iff_eq, decide_eq_decide]
omega
· simp only [mod_two_ne_zero] at h
simp only [h, xor_mod_two_eq_one]
Expand Down

0 comments on commit ba27a19

Please sign in to comment.