[Merged by Bors] - chore(MeasureTheory/Function/ConditionalExpectation): remove unneeded lpMeasSubgroup_coe and lpMeas_coe#22214
Closed
JovanGerb wants to merge 1 commit intomasterfrom lpMeas_coe
+15-32
lpMeasSubgroup_coe and lpMeas_coe#22214