Commit 2025-03-01 01:15 93ddb45c

View on Github →

chore: split Probability/Kernel/Composition/Basic (#22400) New files:

  • Comp: composition of kernels
  • CompProd: composition-product
  • MapComap: map, comap and particular cases like fst and snd
  • CompMap: lemmas about composition and map/comap
  • Prod: product of kernels In order to prove instances for the composition of kernels directly (instead of using the compProd instances), I had to add comp_sum_left, comp_sum_right and comp_apply_univ_le. Apart from that, I only move material around.

Estimated changes