Commit 2025-09-25 07:46 71604a9f

Refactor(Probability/Kernel): build compProd from comp and parallelComp (#29704) This PR changes the definitions of Kernel.compProd and Kernel.prod.

• Before this PR, we had 3 types of compositions of kernels that were built "from scratch": comp, parallelComp and compProd. And then prod was defined using compProd.
• After this PR, only comp and parallelComp are basic blocks of the compositions/products of kernels: compProd and prod are built from those (and from particular deterministic kernels). The auxiliary definition compProdFun that was used only to build compProd is deleted. I had to move several lemmas around to reflect changes in the import structure in the folder. The PR summary bot comment shows that nothing was lost besides results about compProdFun.