mathlib
698c80e9 - chore(probability/kernel/composition): swap the order of the arguments of prod_mk_left (#18929)

Commit
2 years ago
chore(probability/kernel/composition): swap the order of the arguments of prod_mk_left (#18929) Since `prod_mk_left γ κ` creates a `kernel (γ × α) β` from `κ : kernel α β`, it makes more sense to put the `γ` argument to the left.
Author
Parents
Loading