Commit 2025-03-04 13:59 57eb542c

chore(Probability/Kernel): make parallelProd independent of compProd (#22428) The definition of parallelProd used Kernel.prod, which uses compProd. In order to untangle those definitions (and perhaps redefine compProd from comp and parallelProd in the future) this PR replaces the definition of parallelProd by a direct definition. A few lemmas that are about the interaction of parallelProd and other composition or product operations are moved to the Lemmas file to reduce imports.