From c281d78d1de8a1d3a22cd96e2682f6de7f3fefbd Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Fri, 26 Jun 2026 10:49:16 -0500
Subject: [PATCH] Add documentation for IterProd

---
 lean/Spa/Lattice/IterProd.lean | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/lean/Spa/Lattice/IterProd.lean b/lean/Spa/Lattice/IterProd.lean
index 6ebe692..ca442c3 100644
--- a/lean/Spa/Lattice/IterProd.lean
+++ b/lean/Spa/Lattice/IterProd.lean
@@ -1,6 +1,24 @@
 import Spa.Lattice.Prod
 import Spa.Lattice.Unit
 
+/-!
+
+# Iterated Products
+
+Given two types $\alpha$ and $\beta$ and a number $n$, produces
+an iterated product:
+
+$$
+\overbrace{\alpha \times \ldots \times \alpha}^{n\ \text{times}} × \beta
+$$
+
+This is mostly a stepping stone for isomorphisms. In
+`Spa/Lattice/Prod.lean`, By decomposing types such as `Fin n → α` into
+`IterProd α PUnit n`, we can automatically get a proof of their finite
+height via `Spa.FiniteHeightLattice.transport`.
+
+-/
+
 namespace Spa
 
 universe u