Commit 2025-08-04 07:37 1f48e1a8

View on Github →

feat(Probability): lemmas about Kernel.discard (#27584)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/GiryMonad.lean

added theorem Measurable.smul_measure

Modified Mathlib/Probability/Kernel/Basic.lean

added theorem ProbabilityTheory.Kernel.discard_eq_const

Modified Mathlib/Probability/Kernel/Composition/Comp.lean

added theorem ProbabilityTheory.Kernel.comp_discard'

Modified Mathlib/Probability/Kernel/Composition/MeasureComp.lean

added theorem MeasureTheory.Measure.discard_comp