Theorem MeasureTheory.Measure.compProd_smul_left

Modification history

2024-11-28 16:12
Mathlib/Probability/Kernel/MeasureCompProd.lean
feat(Probability): lemmas about composition-product of a measure and a kernel (#19562) …
Added MeasureTheory.Measure.compProd_smul_leftView on Github →