Theorem measurable_toAdd

Modification history

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