doc(set_theory/ordinal/cantor_normal_form): implementation notes (#15466

)

We write a short paragraph on why `CNF` is implemented as a list of pairs.

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