diff --git a/src/set_theory/ordinal/cantor_normal_form.lean b/src/set_theory/ordinal/cantor_normal_form.lean
index 78008de0abc34..518de3a42febb 100644
--- a/src/set_theory/ordinal/cantor_normal_form.lean
+++ b/src/set_theory/ordinal/cantor_normal_form.lean
@@ -11,7 +11,16 @@ import set_theory.ordinal.arithmetic
 
 The Cantor normal form of an ordinal is generally defined as its base `ω` expansion, with its
 non-zero exponents in decreasing order. Here, we more generally define a base `b` expansion
-`ordinal.CNF` in this manner, for any `b ≥ 2`.
+`ordinal.CNF` in this manner, which is well-behaved for any `b ≥ 2`.
+
+# Implementation notes
+
+We implement `ordinal.CNF` as an association list, where keys are exponents and values are
+coefficients. This is because this structure intrinsically reflects two key properties of the Cantor
+normal form:
+
+- It is ordered.
+- It has finitely many entries.
 
 # Todo