Commit 2024-05-28 12:13 e0685aa8

View on Github →

feat: add mul_iff right and mul_iff_left for (AE)(Strongly)Measurable (#12711) Add the lemma that says that if f is measurable, then f+g is measurable iff g is measurable. Then add the same but with g+f, and the same lemmas about AEMeasurable, StronglyMeasurable and AEStronglyMeasurable.

Estimated changes