Theorems · Theorem · number theory
Nat.xor_range
∀ (n : ℕ),
List.foldl (fun x1 x2 => x1 ^^^ x2) 0 (List.range (n + 1)) =
match Fin.ofNat 4 n with
| 0 => n
| 1 => 1
| 2 => n + 1
| 3 => 0The xor of the numbers from 0 to n can be easily calculated using n mod 4.
- Defined in
- Mathlib.Data.Nat.Bitwise
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 53 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- zero_addproof · cited by 2,366
- Nat.even_iffproof · cited by 8
- Nat.xor_one_of_evenproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.