Theorem MeasureTheory.AEStronglyMeasurable.mul_iff_right

Modification history

2025-01-25 09:32

Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

refactor: merge `AEStronglyMeasurable` and `AEStronglyMeasurable'` (#20932) …

Modified MeasureTheory.AEStronglyMeasurable.mul_iff_right View on Github →

2024-05-28 12:13

Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

feat: add mul_iff right and mul_iff_left for (AE)(Strongly)Measurable (#12711) …

Added MeasureTheory.AEStronglyMeasurable.mul_iff_right View on Github →