diff --git a/Mathlib/Probability/Independence/Basic.lean b/Mathlib/Probability/Independence/Basic.lean
index 2123ec8693a88c..89e4c252093048 100644
--- a/Mathlib/Probability/Independence/Basic.lean
+++ b/Mathlib/Probability/Independence/Basic.lean
@@ -1011,6 +1011,12 @@ theorem iIndepSet.iIndepFun_indicator [Zero β] [One β] {m : MeasurableSpace β
     iIndepFun (fun n => (s n).indicator fun _ω => (1 : β)) μ :=
   Kernel.iIndepSet.iIndepFun_indicator hs
 
+lemma Indep.indicator_indepFun {m : MeasurableSpace Ω} {M 𝓧 : Type*}
+    [Zero M] [MeasurableSpace M] (c : M) [NeZero c] {m𝓧 : MeasurableSpace 𝓧} {A : Set Ω}
+    {X : Ω → 𝓧} (hA : MeasurableSet[m] A) (h : Indep m (m𝓧.comap X) μ) :
+    (A.indicator (fun _ ↦ c)) ⟂ᵢ[μ] X :=
+  Kernel.Indep.indicator_const_indepFun c hA h
+
 end IndepFun
 
 variable {ι Ω α β : Type*} {mΩ : MeasurableSpace Ω} {mα : MeasurableSpace α}
diff --git a/Mathlib/Probability/Independence/Kernel/IndepFun.lean b/Mathlib/Probability/Independence/Kernel/IndepFun.lean
index 8b0aa910023026..957fd84de29e9b 100644
--- a/Mathlib/Probability/Independence/Kernel/IndepFun.lean
+++ b/Mathlib/Probability/Independence/Kernel/IndepFun.lean
@@ -694,6 +694,12 @@ theorem iIndepSet.iIndepFun_indicator [Zero β] [One β] {m : MeasurableSpace β
   · exact @MeasurableSet.empty _ (generateFrom {s i})
   · exact @MeasurableSet.empty _ (generateFrom {s i})
 
+lemma Indep.indicator_const_indepFun {m : MeasurableSpace Ω} {M 𝓧 : Type*}
+    [Zero M] [MeasurableSpace M] (c : M) [NeZero c] {m𝓧 : MeasurableSpace 𝓧} {A : Set Ω}
+    {X : Ω → 𝓧} (hA : MeasurableSet[m] A) (h : Indep m (m𝓧.comap X) κ μ) :
+    IndepFun (A.indicator (fun _ ↦ c)) X κ μ :=
+  indep_of_indep_of_le_left h (measurable_const.indicator hA).comap_le
+
 variable {mβ : MeasurableSpace β} {X : ι → Ω → α} {Y : ι → Ω → β}
   {f : _ → Set Ω} {t : ι → Set β} {s : Finset ι}