mathlib3

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

#1259

Merged