ProbabilityTheory.Kernel.rdist_zero_kernel_right

@[simp] lemma rdist_zero_kernel_right {κ : Kernel T G} [IsFiniteKernel κ]    {μ : Measure T} {ν : Measure T'} [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]    [FiniteSupport μ] [FiniteSupport ν] :    dk[κ ; μ # 0 ; ν] = - Hk[κ, μ] / 2 := by  rw [rdist_eq']  simp only [prodMkLeft_zero, entropy_zero_kernel, zero_div, sub_zero]  rw [sub_eq_iff_eq_add]  ring_nf  have : map (prodMkRight T' κ ×ₖ (0 : Kernel (T × T') G)) (fun x ↦ x.1 - x.2)      = 0 := by    ext1 x    rw [map_apply _ (by fun_prop), prod_apply]    simp  rw [this, entropy_zero_kernel]