Theorem MeasureTheory.Measure.discard_comp

Modification history

2025-08-04 07:37
Mathlib/Probability/Kernel/Composition/MeasureComp.lean
feat(Probability): lemmas about `Kernel.discard` (#27584)
Added MeasureTheory.Measure.discard_compView on Github →