mathlib

e3d9adf1 - chore(measure_theory/function/conditional_expectation): change condexp notation (#10584)

chore(measure_theory/function/conditional_expectation): change condexp notation (#10584) The previous definition and notation showed the `measurable_space` argument only through the other argument `m \le m0`, which tends to be replaced by `_` in the goal view if it becomes complicated.