Theorem aestronglyMeasurable_smul_iff

Modification history

2026-08-05 23:02
Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
feat: multiplying by an almost-everywhere invertible scalar function preserves a.e. strong measurability (#42445) …
Added aestronglyMeasurable_smul_iffView on Github →