Commit 2023-09-27 15:18 b42cde1f

View on Github →

feat(Probability/Kernel): add simp lemmas about the zero kernel (#7381)

Estimated changes

Modified Mathlib/Probability/Kernel/Composition.lean

added theorem ProbabilityTheory.kernel.comap_zero

added theorem ProbabilityTheory.kernel.compProd_zero_left

added theorem ProbabilityTheory.kernel.compProd_zero_right

added theorem ProbabilityTheory.kernel.map_zero