composition): redefine kernel.comp using measure.bind, remove kernel.map_measure
#19160

Closed

[Merged by Bors] - chore(probability/kernel/composition): redefine kernel.comp using measure.bind, remove kernel.map_measure #19160

RemyDegenne wants to merge 2 commits into master from RD_comp_is_bind

comp is bind

7aa03821

RemyDegenne added awaiting-review

RemyDegenne added t-measure-probability

RemyDegenne requested a review 2 years ago

RemyDegenne requested a review from

kex-y 2 years ago

sgouezel commented on 2023-06-07

leanprover-community-bot-assistant added delegated

leanprover-community-bot-assistant removed awaiting-review

fix docstring

057ef4ce

github-actions added ready-to-merge

bors changed the title ~~chore(probability/kernel/composition): redefine kernel.comp using measure.bind, remove kernel.map_measure~~ [Merged by Bors] - chore(probability/kernel/composition): redefine kernel.comp using measure.bind, remove kernel.map_measure 2 years ago

bors closed this 2 years ago

bors deleted the RD_comp_is_bind branch 2 years ago

Reviewers

sgouezel

kex-y

Assignees

No one assigned

Labels

ready-to-merge delegated t-measure-probability

Milestone

No milestone

mathlib3 [Merged by Bors] - chore(probability/kernel/composition): redefine kernel.comp using measure.bind, remove kernel.map_measure #19160 Closed

[Merged by Bors] - chore(probability/kernel/composition): redefine kernel.comp using measure.bind, remove kernel.map_measure #19160

mathlib3
[Merged by Bors] - chore(probability/kernel/composition): redefine kernel.comp using measure.bind, remove kernel.map_measure
#19160

Closed