chore: fix docstring (#21027)

leanprover-community · Jan 24, 2025 · 59eed68 · 59eed68
1 parent 725eddc
commit 59eed68
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean b/Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean
@@ -198,8 +198,8 @@ theorem ae_eq_of_integral_contDiff_smul_eq
     (fun g g_diff g_supp ↦ h g g_diff.contDiff g_supp)
 
 /-- If a function `f` locally integrable on an open subset `U` of a finite-dimensional real
-  manifold has zero integral when multiplied by any smooth function compactly supported
-  in an open set `U`, then `f` vanishes almost everywhere in `U`. -/
+  vector space has zero integral when multiplied by any smooth function compactly supported
+  in `U`, then `f` vanishes almost everywhere in `U`. -/
 theorem IsOpen.ae_eq_zero_of_integral_contDiff_smul_eq_zero {U : Set E} (hU : IsOpen U)
     (hf : LocallyIntegrableOn f U μ)
     (h : ∀ (g : E → ℝ), ContDiff ℝ ∞ g → HasCompactSupport g → tsupport g ⊆ U →