Theorem measurableSet_preimage_toMul

Modification history

2026-11-10 23:17
Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean
feat({Topology,MeasureTheory}): instances for `Additive`/`Multiplicative` (#45174) …
Added measurableSet_preimage_toMulView on Github →