Def MeasurableEquiv.multiplicative

Modification history

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