diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
index 825e8ed1dffd..4b75b8ec87d7 100644
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -15,6 +15,9 @@ the `Fin 2^n` representation and Boolean vectors.  It is still under development
 intended to provide a path for converting SAT and SMT solver proofs about BitVectors
 as vectors of bits into proofs about Lean `BitVec` values.
 
+The module is named for the bit-blasting operation in an SMT solver that converts bitvector
+expressions into expressions about individual bits in each vector.
+
 ### Example: How bitblasting works for multiplication
 
 We explain how the lemmas here are used for bitblasting,