mathlib4#34521 & mathlib4#34435 (Probability/MeasureTheory)

Stream: PR reviews

[huaizhangchu]

Hi everyone, I'm bumping two related PRs that have been awaiting review. Both have green CI.

• mathlib4#34521: feat(MeasureTheory): add measurableEmbedding_natCast. This is a small, self-contained lemma needed for the next PR. Assigned to @Kexing Ying .
• mathlib4#34435: feat(Probability): convolution of Poisson distributions. Proves Poisson(r1)∗Poisson(r2)=Poisson(r1​+r2​) using characteristic functions. It depends on #34521. Assigned to @Rémy Degenne .
  Any feedback would be greatly appreciated. Thank you!