Commit 2025-10-08 08:14 c32a3cfc

feat(Probability): existence of independent random variables with a given sequence of distributions (#29959) In some sense none of these are necessary, especially exists_hasLaw, because one could just use the identity or the projections of the product explicitly, but I think using these lemmas when one wants to introduce random variables in probabilistic proofs will be much more natural. Also added needed fun_prop tags to aemeasurable_id lemmas which randomly generalized charFun_map_smul to not need SecondCountableTopology (detected by the linter).