Mathlib v3 is deprecated. Go to Mathlib v4

Theorem probability_theory.kernel.comp_eq_snd_comp_prod

Modification history

2023-06-07 11:35
src/probability/kernel/composition.lean
chore(probability/kernel/composition): redefine kernel.comp using measure.bind, remove kernel.map_measure (#19160) …
Added probability_theory.kernel.comp_eq_snd_comp_prodView on Github →