Commit 2025-03-06 11:11 09a79323

feat: Giry monoidal product (#22062) Description: Proves that the monoidal product of the Giry monoidal monad is measurable, following Lemma 4.1 https://doi.org/10.1016/j.aim.2020.107239 The file MeasureTheory/Measure/Prod.lean proves that partial applications of Prod.mk are measurable (eg. Measurable.map_prod_mk_left) but this does not suffice to show that Prod.mk is a measurable function out of both arguments at once. Therefore, this lemma is useful for doing monadic probability theory without using Markov kernels. I'm a first-time contributor, so feedback is very welcome :)