Commit 2025-01-22 10:59 03251ae0
View on Github →feat: μ[f * g | m] =ᵐ[μ] μ[f | m] * g if g is strongly m-measurable (#20928)
This is a corollary of the lemma with opposite multiplication.
Also rename the existing variant to better follow the naming convention and be more discoverable.
From my PhD (LeanCamCombi)