https://github.com/math-comp/analysis/blob/673e9082f732e81b4d518ec21d47c198a237199c/theories/measure_theory/measurable_structure.v#L940 ```coq HB.instance Definition _ d d' (X : pmeasurableType d) (Y : pmeasurableType d') := Measurable.on (X * Y)%type. ```
analysis/theories/measure_theory/measurable_structure.v
Line 940 in 673e908
HB.instance Definition _ d d' (X : pmeasurableType d) (Y : pmeasurableType d') := Measurable.on (X * Y)%type.