diff --git a/Mathlib/Probability/Kernel/Composition/Basic.lean b/Mathlib/Probability/Kernel/Composition/Basic.lean
index 8fd4daf2faf96..17ca21091f0e6 100644
--- a/Mathlib/Probability/Kernel/Composition/Basic.lean
+++ b/Mathlib/Probability/Kernel/Composition/Basic.lean
@@ -1061,6 +1061,104 @@ lemma snd_swapRight (κ : Kernel α (β × γ)) : snd (swapRight κ) = fst κ :=
 
 end FstSnd
 
+section sectLsectR
+
+variable {γ δ : Type*} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ}
+
+/-- Define a `Kernel α γ` from a `Kernel (α × β) γ` by taking the comap of `fun a ↦ (a, b)` for
+a given `b : β`. -/
+noncomputable def sectL (κ : Kernel (α × β) γ) (b : β) : Kernel α γ :=
+  comap κ (fun a ↦ (a, b)) (measurable_id.prod_mk measurable_const)
+
+@[simp] theorem sectL_apply (κ : Kernel (α × β) γ) (b : β) (a : α) : sectL κ b a = κ (a, b) := rfl
+
+@[simp] lemma sectL_zero (b : β) : sectL (0 : Kernel (α × β) γ) b = 0 := by simp [sectL]
+
+instance (κ : Kernel (α × β) γ) (b : β) [IsMarkovKernel κ] : IsMarkovKernel (sectL κ b) := by
+  rw [sectL]; infer_instance
+
+instance (κ : Kernel (α × β) γ) (b : β) [IsZeroOrMarkovKernel κ] :
+    IsZeroOrMarkovKernel (sectL κ b) := by
+  rw [sectL]; infer_instance
+
+instance (κ : Kernel (α × β) γ) (b : β) [IsFiniteKernel κ] : IsFiniteKernel (sectL κ b) := by
+  rw [sectL]; infer_instance
+
+instance (κ : Kernel (α × β) γ) (b : β) [IsSFiniteKernel κ] : IsSFiniteKernel (sectL κ b) := by
+  rw [sectL]; infer_instance
+
+instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((sectL κ b) a) := by
+  rw [sectL_apply]; infer_instance
+
+instance (priority := 100) {κ : Kernel (α × β) γ} [∀ b, IsMarkovKernel (sectL κ b)] :
+    IsMarkovKernel κ := by
+  refine ⟨fun _ ↦ ⟨?_⟩⟩
+  rw [← sectL_apply, measure_univ]
+
+--I'm not sure this lemma is actually useful
+lemma comap_sectL (κ : Kernel (α × β) γ) (b : β) {f : δ → α} (hf : Measurable f) :
+    comap (sectL κ b) f hf = comap κ (fun d ↦ (f d, b)) (hf.prod_mk measurable_const) := by
+  ext d s
+  rw [comap_apply, sectL_apply, comap_apply]
+
+@[simp]
+lemma sectL_prodMkLeft (α : Type*) [MeasurableSpace α] (κ : Kernel β γ) (a : α) {b : β} :
+    sectL (prodMkLeft α κ) b a = κ b := rfl
+
+@[simp]
+lemma sectL_prodMkRight (β : Type*) [MeasurableSpace β] (κ : Kernel α γ) (b : β) :
+    sectL (prodMkRight β κ) b = κ := rfl
+
+/-- Define a `Kernel β γ` from a `Kernel (α × β) γ` by taking the comap of `fun b ↦ (a, b)` for
+a given `a : α`. -/
+noncomputable def sectR (κ : Kernel (α × β) γ) (a : α) : Kernel β γ :=
+  comap κ (fun b ↦ (a, b)) (measurable_const.prod_mk measurable_id)
+
+@[simp] theorem sectR_apply (κ : Kernel (α × β) γ) (b : β) (a : α) : sectR κ a b = κ (a, b) := rfl
+
+@[simp] lemma sectR_zero (a : α) : sectR (0 : Kernel (α × β) γ) a = 0 := by simp [sectR]
+
+instance (κ : Kernel (α × β) γ) (a : α) [IsMarkovKernel κ] : IsMarkovKernel (sectR κ a) := by
+  rw [sectR]; infer_instance
+
+instance (κ : Kernel (α × β) γ) (a : α) [IsZeroOrMarkovKernel κ] :
+    IsZeroOrMarkovKernel (sectR κ a) := by
+  rw [sectR]; infer_instance
+
+instance (κ : Kernel (α × β) γ) (a : α) [IsFiniteKernel κ] : IsFiniteKernel (sectR κ a) := by
+  rw [sectR]; infer_instance
+
+instance (κ : Kernel (α × β) γ) (a : α) [IsSFiniteKernel κ] : IsSFiniteKernel (sectR κ a) := by
+  rw [sectR]; infer_instance
+
+instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((sectR κ a) b) := by
+  rw [sectR_apply]; infer_instance
+
+instance (priority := 100) {κ : Kernel (α × β) γ} [∀ b, IsMarkovKernel (sectR κ b)] :
+    IsMarkovKernel κ := by
+  refine ⟨fun _ ↦ ⟨?_⟩⟩
+  rw [← sectR_apply, measure_univ]
+
+--I'm not sure this lemma is actually useful
+lemma comap_sectR (κ : Kernel (α × β) γ) (a : α) {f : δ → β} (hf : Measurable f) :
+    comap (sectR κ a) f hf = comap κ (fun d ↦ (a, f d)) (measurable_const.prod_mk hf) := by
+  ext d s
+  rw [comap_apply, sectR_apply, comap_apply]
+
+@[simp]
+lemma sectR_prodMkLeft (α : Type*) [MeasurableSpace α] (κ : Kernel β γ) (a : α) :
+    sectR (prodMkLeft α κ) a = κ := rfl
+
+@[simp]
+lemma sectR_prodMkRight (β : Type*) [MeasurableSpace β] (κ : Kernel α γ) (b : β) {a : α} :
+    sectR (prodMkRight β κ) a b = κ a := rfl
+
+@[simp] lemma sectL_swapRight (κ : Kernel (α × β) γ) : sectL (swapLeft κ) = sectR κ := rfl
+
+@[simp] lemma sectR_swapRight (κ : Kernel (α × β) γ) : sectR (swapLeft κ) = sectL κ := rfl
+
+end sectLsectR
+
 section Comp
 
 /-! ### Composition of two kernels -/
@@ -1202,6 +1300,7 @@ variable {γ δ : Type*} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ}
 noncomputable def prod (κ : Kernel α β) (η : Kernel α γ) : Kernel α (β × γ) :=
   κ ⊗ₖ swapLeft (prodMkLeft β η)
 
+@[inherit_doc]
 scoped[ProbabilityTheory] infixl:100 " ×ₖ " => ProbabilityTheory.Kernel.prod
 
 theorem prod_apply' (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsSFiniteKernel η]
diff --git a/Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean b/Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
index b57ca2ef11459..64933b8111dc2 100644
--- a/Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
+++ b/Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
@@ -73,6 +73,14 @@ lemma compProd_apply_prod [SFinite μ] [IsSFiniteKernel κ]
   rw [indicator_apply]
   split_ifs with ha <;> simp [ha]
 
+lemma _root_.ProbabilityTheory.Kernel.compProd_apply_eq_compProd_sectR {γ : Type*}
+    {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : Kernel (α × β) γ)
+    [IsSFiniteKernel κ] [IsSFiniteKernel η] (a : α) :
+    (κ ⊗ₖ η) a = (κ a) ⊗ₘ (Kernel.sectR η a) := by
+  ext s hs
+  simp_rw [Kernel.compProd_apply hs, compProd_apply hs, Kernel.sectR_apply]
+  rfl
+
 lemma compProd_congr [IsSFiniteKernel κ] [IsSFiniteKernel η]
     (h : κ =ᵐ[μ] η) : μ ⊗ₘ κ = μ ⊗ₘ η := by
   by_cases hμ : SFinite μ