diff --git a/Clt/CharFun.lean b/Clt/CharFun.lean
index 0d654c8..0a9651c 100644
--- a/Clt/CharFun.lean
+++ b/Clt/CharFun.lean
@@ -69,6 +69,7 @@ namespace ProbabilityTheory
 
 variable {E : Type*} [MeasurableSpace E]
 
+/-- The characteristic function of a measure. -/
 noncomputable
 def charFun [Inner ℝ E] (μ : Measure E) (t : E) : ℂ := ∫ x, exp (⟪t, x⟫ • I) ∂μ