diff --git a/Batteries/Data/Nat/Bitwise.lean b/Batteries/Data/Nat/BinaryRec.lean
similarity index 89%
rename from Batteries/Data/Nat/Bitwise.lean
rename to Batteries/Data/Nat/BinaryRec.lean
index 1db0a426e2..91bef32a5a 100644
--- a/Batteries/Data/Nat/Bitwise.lean
+++ b/Batteries/Data/Nat/BinaryRec.lean
@@ -1,7 +1,19 @@
 /-
-Copyright (c) 2024 Yuyang Zhao. All rights reserved.
+Copyright (c) 2022 Praneeth Kolichala. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yuyang Zhao
+Authors: Praneeth Kolichala, Yuyang Zhao
+-/
+
+/-!
+# Binary recursion on `Nat`
+
+This file defines binary recursion on `Nat`.
+
+## Main results
+* `Nat.binaryRec`: A recursion principle for `bit` representations of natural numbers.
+* `Nat.binaryRec'`: The same as `binaryRec`, but the induction step can assume that if `n=0`,
+  the bit being appended is `true`.
+* `Nat.binaryRecFromOne`: The same as `binaryRec`, but special casing both 0 and 1 as base cases.
 -/
 
 namespace Nat