mathlib3
feat(measure_theory): prove that the Giry monad is a monad in the category_theory sense
#1259

Merged

feat(measure_theory): prove that the Giry monad is a monad in the category_theory sense #1259

mergify merged 7 commits into master from giry_monad

johoelzl requested a review 6 years ago

jcommelin commented on 2019-07-24

feat(measure_theory): prove that the Giry monad is a monad in the cat…

74b1327a

johoelzl force pushed from dba8c646 to 74b1327a 6 years ago

jcommelin commented on 2019-07-24

Add spaces to fix alignment

e9bdeb32

jcommelin commented on 2019-07-24

Merge branch 'master' into giry_monad

fee6949e

document Measure

707832d7

robertylewis added needs-documentation

cipher1024 assigned

rwbarton 6 years ago

Add documentation

c9686988

rwbarton removed needs-documentation

rwbarton unassigned

rwbarton 6 years ago

Merge remote-tracking branch 'origin/master' into HEAD

a239f5f7

jcommelin commented on 2019-09-03

Add space before colon

de52f18f

jcommelin approved these changes on 2019-09-03

jcommelin added ready-to-merge

mergify merged ff47fa31 into master 6 years ago

mergify deleted the giry_monad branch 6 years ago

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone