Commit 2025-01-25 09:32 319694c0
View on Github →refactor: merge AEStronglyMeasurable and AEStronglyMeasurable' (#20932)
AEStronglyMeasurable is a convenient special case of AEStronglyMeasurable', but we can tweak the argument implicitness so that AEStronglyMeasurable f μ means the same thing as before while AEStronglyMeasurable[m] f μ means the same thing as the current AEStronglyMeasurable' m f μ.